assert semantic change proposal
via Digitalmars-d
digitalmars-d at puremagic.com
Wed Aug 6 12:18:29 PDT 2014
On Wednesday, 6 August 2014 at 18:51:05 UTC, Ola Fosheim Grøstad
wrote:
> On Wednesday, 6 August 2014 at 17:59:06 UTC, Marc Schütz wrote:
>> The crux is the axiom that is being defined. When you write
>> `assume(condition)`, the axiom is not:
>>
>> "`condition` is true."
>>
>> but:
>>
>> "When control flow reaches this point, then `condition` is
>> true."
>>
>> It's not an unconditionally true condition :-P
>
> Assume(X) does not provide a condition. It defines a
> proposition/relation to be true.
Well, let's call it proposition then...
>
> If you define a relation between two constants then it has to
> hold globally. Otherwise they are not constant…
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.
>
> Assume(P) defines that the proposition holds. If it does not
> involve variables, then it will be free to move anywhere by the
> rules of Hoare-logic (and propositional logic)? If
> assume(PI==3.14…) can move everywhere, by the rules, then so
> can assume(true==false).
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".
>
> You surely don't want to special case "true==false" in the
> hoare logic rules?
>
> Please note that it is perfectly fine to define "true==false",
> but you then have to live by it, that is, you no longer have a
> boolean algebra, you have an unsound algebra. And that holds
> globally. So, please don't think that assume(true==false) is a
> test of a condition, it is just a definition that you impose on
> the equality relation (that also, by incident, happens to make
> the algebra unsound)
>
> If you special case assume(false) and assert(false) then you
> can no longer use deduction properly and it essentially becomes
> an aberration, syntactical sugar, that needs special casing
> everywhere.
>
> It would be much better to just halt compilation if you at
> compile time can evaluate X==false for assume(X) or assert(X).
> Why let this buggy code live? If it failed at compile time then
> let the compilation fail! This would work better with CTFE.
>
> "@unreachable" is an alternative if you want to be explicit
> about it and matches __builtin_unreachable et al.
See above, no special treatment is necessary.
More information about the Digitalmars-d
mailing list