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?
This is an assume, not an assert. The user tells the compiler
that `running` is false after the loop, it can thus conclude that
the loop will never run. So there is no non-terminating loop in
this case.
