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?
But I was talking about explicit assumptions made by the
programmer, who does not know the rules… It was obviously wrong
to assume anything to hold if the loop never terminates.
The rule for proving loop termination is quite involved where you
basically prove that every time you move through the loop you
get something "less" than you had before (ensured by t and D).
This is no fun, and a good reason to hate reasoning about
correctness:
a < b: is a well-founded ordering on the set D
if this holds:
[P ∧ B ∧ t ∈ D ∧ t = z] S [P ∧ t ∈ D ∧ t < z ]
then this holds:
[P ∧ t ∈ D] while B do S done [¬B ∧ P ∧ t ∈ D]
I think… or maybe not. Who can tell from just glancing at it?
