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.
