assert semantic change proposal

[David Bregman via Digitalmars-d]

On Thursday, 7 August 2014 at 07:53:44 UTC, Ola Fosheim Grøstad 
wrote:
> On Thursday, 7 August 2014 at 06:04:38 UTC, David Bregman wrote:
>> On Thursday, 7 August 2014 at 03:54:12 UTC, Ola Fosheim 
>> Grøstad wrote:
>>> «The __assume(0) statement is a special case.»
>>>
>>> So, it does not make perfect sense. If it did, it would not 
>>> be a special case?
>>
>> It doesn't have to be a special case if you define it in the 
>> right way - in terms of control flow. Then the interpretation 
>> of assume(false) as unreachable follows quite naturally:
>>
>> instead of defining assume(x) to mean that x is an axiom, 
>> define assume(x) to mean that P=>x is an axiom, where P is the 
>> proposition that control flow reaches the assume statement.
>>
>> so assume(false) actually means P=>false, or simply !P
>>
>> and !P means !(control flow reaches the assume), as desired.
>
> Let's try the opposite way instead:
>
> assume(Q)
> if(B1){
>    if(B2){
>    }
> }
>
> implies:
>
> assume(Q)
> if(B1){
>    assume(B1&&Q)
>    if(B2){
>       assume(B1&&B2&&Q)
>    }
> }
>
> So your P in the inner if statement is  B1&&B2.
>
> However assume(P&&false) is still a fallacy…
>
> Or?

If you use the definition of assume that I gave, assume(P && 
false) declares the axiom

P => (P && false)

which is again equivalent to !P.