assert semantic change proposal

David Bregman via Digitalmars-d digitalmars-d at puremagic.com
Thu Aug 7 10:38:21 PDT 2014


On Thursday, 7 August 2014 at 16:56:01 UTC, Ola Fosheim Grøstad 
wrote:
> On Thursday, 7 August 2014 at 16:36:09 UTC, David Bregman wrote:
>> Right. So if X is false, the axiom we declare is !P, not 
>> "false" or "a fallacy".
>
> But Pn is always true where you assume…?

No. Remember P is "control flow can reach this assume". If the 
assume is unreachable, then P is false. The compiler doesn't 
always know that P is false though, so we can use assume(false) 
to supply that as an axiom.

Here's an example:

x = rand() & 3; // x is 0,1,2 or 3.
switch(x) {
   case 0: foo();
   case 1: bar();
   case 2: baz();
   case 3: qux();
   default: assume(false); // hopefully redundant with a decent 
compiler.
}

now the compiler can optimize this down to

{foo, bar, baz, qux}[x]();

or even better, a computed jump.

>
>> False => X is true for any X, so the axiom we declare is just 
>> a tautology.
>
> I don't follow. If any assumption is false then anything goes…
>

Using my definition of assume, the axiom declared is P=>x. If P 
is false, then the axiom declared is false => x, which is true 
for any x.

http://en.wikipedia.org/wiki/Truth_table#Logical_implication


>> So is the control flow definition / unreachability argument 
>> clear now?
>
> Nope.

Ok, is it clear now? If not, which parts are not clear?



More information about the Digitalmars-d mailing list