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