assert semantic change proposal

via Digitalmars-d digitalmars-d at puremagic.com
Wed Aug 6 08:29:12 PDT 2014


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?


More information about the Digitalmars-d mailing list