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