On Wednesday, 6 August 2014 at 15:29:13 UTC, Ola Fosheim Grøstad
wrote:
On Wednesday, 6 August 2014 at 15:02:10 UTC, Matthias Bentrup
wrote:
is equivalent to
while(running) {
...don't assign to running, don't break...
}
assume(!running);
You have to prove termination to get there? Plain Hoare logic
cannot deal with non-terminating loops. Otherwise you risk
proving any theorem below the loop to hold?
I'm pretty sure that running is false when the program reaches
the end of the while loop, whether it is assigned in the loop or
not. I only added the "don't assign to running" to make the
example match your pattern.
