assert semantic change proposal

[Matthias Bentrup via Digitalmars-d]

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?
>

I'm pretty sure that running is false when the program reaches
the end of the while loop, whether it is assigned in the loop or
not. I only added the "don't assign to running" to make the
example match your pattern.