assert semantic change proposal

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

This is an assume, not an assert. The user tells the compiler 
that `running` is false after the loop, it can thus conclude that 
the loop will never run. So there is no non-terminating loop in 
this case.