assert semantic change proposal

[David Bregman via Digitalmars-d]

On Thursday, 7 August 2014 at 15:35:30 UTC, Ola Fosheim Grøstad 
wrote:
> On Thursday, 7 August 2014 at 14:09:26 UTC, David Bregman wrote:
>> If you use the definition of assume that I gave, assume(P && 
>> false) declares the axiom
>>
>> P => (P && false)
>>
>> which is again equivalent to !P.
>
> Well, P=>(P&&X) is equivalent to P=>X.

Right. So if X is false, the axiom we declare is !P, not "false" 
or "a fallacy".

> But you are allowed to have "false" in the preconditions, since 
> we only are interested in
>
> preconditions => postconditions

That's ok. There is no contradiction if P is false.

False => X is true for any X, so the axiom we declare is just a 
tautology.


So is the control flow definition / unreachability argument clear 
now?


> > assume(input!=0) is ok… it does not say unreachable.
> > It says, postconditions are not required to hold for input==0…

> And… assume(false) is a precondition that says that you don't 
> have to care about the postconditions at all… Basically, 
> "assume anything"…

I don't get this part, maybe you can reword it if I haven't 
already answered the question.