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