assert semantic change proposal

[via Digitalmars-d]

On Wednesday, 6 August 2014 at 19:18:30 UTC, Marc Schütz wrote:
> On Wednesday, 6 August 2014 at 18:51:05 UTC, Ola Fosheim

> Yes, but as I wrote above, we're not defining a relation 
> between two constants ("true == false"), we define the 
> following axiom:
>
>     "When control flow reaches this point, then true == false."
>
> Because true is not equal to false, it follows that the first 
> part of the proposition cannot be true, meaning control flow 
> will not reach this point.

But you are defining an axiom, not evaluating, that is how the 
optimizer can use it for deduction. Think of how Prolog works.

> See above. Of course we could define our `assume(P)` to define 
> `P` as an axiom directly, but this would be much less useful, 
> because it would have exactly the consequences you write about. 
> And it would be a lot more consistent, too. Surely you wouldn't 
> want `assume(x == 42)` to mean "x is always and everywhere 
> equal to 42", but just "x is equal to 42 when control flow 
> passes this point".

I think there is a misunderstanding here. If you have:

uint x=0;

then that invokes many axioms defined by the language:

uint x=0;
assume(x exists from here)
assume(any value assigned to x has to be in the range 
[0,0xffffffff])
assume(x==0)
assume(type(x)=='uint')
assume(…etc…)

So if you then do:

x=x+1
assert(x==1)

You have to move the assert upwards (3+ steps) and see if it 
satisfied by any of the axioms you run into.

3: assert(x==0) //covered by axiom(x==0), x==1 is satisfied
2: assert(x+1-1==1-1)
1: assert(x+1==1)
x=x+1
assert(x==1)

Without the "uint x=0;" you would then have moved all the way up 
to the global scope (conceptually speaking) and not been able to 
find any axioms matching 'x'.

If you assume(x==0) on the other hand, then you don't need the 
other axioms at all. It is instantly satisfied. No need to prove 
anything.

> See above, no special treatment is necessary.

I don't follow. If you use assert(false) to signify anything 
special beyond requesting a proof or assume(false) for anything 
beyond defining an axiom, then you are special casing.