On Wednesday, 6 August 2014 at 17:08:18 UTC, Ola Fosheim Grøstad
wrote:
On Wednesday, 6 August 2014 at 17:03:44 UTC, Marc Schütz wrote:
I guess we're talking past each other. You were saying that
Hoare logic doesn't work with non-terminating loops, and I was
responding that there was no non-terminating loop in the
example. That's all there is to it.
Oh well, but a terminating loop that does not change the
condition is just an empty statement. So then you have
basically proved that it isn't a loop… ;)
I still can't see how you can infer that the assume(!running)
which clearly holds after the loop also holds before the loop.
