On Wednesday, 6 August 2014 at 16:00:33 UTC, Ola Fosheim Grøstad
wrote:
On Wednesday, 6 August 2014 at 15:36:52 UTC, Marc Schütz wrote:
This is an assume, not an assert.
Not sure what you mean. An assume is an assert proven (or
defined) to hold. It can be a proven theorem which has been
given the status of an axiom. It is known to keep the algebraic
system sound. If you claim that something unsound is proven
then all bets are off everywhere?
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.
To clarify: The assume condition wasn't `false`, it was
`!running`. There is a situation in which this is true, namely
when `running` is false at the point where the assume is. Because
the variable isn't changed in the loop, it follows that it's also
true before the loop. I see no contradiction here.
