assert semantic change proposal

via Digitalmars-d digitalmars-d at puremagic.com
Wed Aug 6 10:03:43 PDT 2014


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.


More information about the Digitalmars-d mailing list