assert semantic change proposal

[via Digitalmars-d]

On Thursday, 7 August 2014 at 16:36:09 UTC, David Bregman wrote:
> Right. So if X is false, the axiom we declare is !P, not 
> "false" or "a fallacy".

But Pn is always true where you assume…?

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

I don't follow. If any assumption is false then anything goes…

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

Nope.

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

assume(true)
r = calc()
assert(specification_test(r)) //required to hold for any situation

assume(false)
r=calc()
//r can be anything


// input!=0
assume(input!=0) // true
r=calc(input)
assert(specification(input)==r) // required to hold for input!=0


//input=0
assume(input!=0)  // false
r=calc(input)
assert(specification(input)==r) // may or may not hold