On Thursday, 7 August 2014 at 17:38:22 UTC, David Bregman wrote:
Using my definition of assume, the axiom declared is P=>x. If P
is false, then the axiom declared is false => x, which is true
for any x.
I don't see how this will work out. If it is truly unreachable
then you don't need any assume, because then you can assert
anything. Therefore you shouldn't.
valid:
assume(true)
while(true){}
assert(angels_love_pixiedust) //proven true now…
But there are alternatives to HL that I don't know much about.
You might want to look at "Matching Logic Reachability". Looks
complicated:
http://fsl.cs.illinois.edu/pubs/rosu-stefanescu-2012-fm.pdf
Ok, is it clear now? If not, which parts are not clear?
It doesn't make any sense to me since I don't see how you would
discriminate between your Ps.
{P1}
while(true) skip; endwhile
{P2}
How do you define P1 and P2 to be different?
