On 08/06/14 10:28, eles via Digitalmars-d wrote: > On Wednesday, 6 August 2014 at 07:29:02 UTC, Ola Fosheim Grøstad wrote: >> On Wednesday, 6 August 2014 at 06:56:40 UTC, eles wrote: > >> Not right: >> >> b = a+1 >> assume(b>C) >> >> implies >> >> assume(a+1>C) >> b = a+1 > > b = a+1 > if(C<=b) exit(1); > > implies > > if(C<=a+1) exit(1); > b = a+1 > > Is not the same? Still, one would allow the optimizer to exit before > executing b=a+1 line (in the first version) based on that condition > (considering no volatile variables).
It is *very* different. In the `exit` case this kind of transformation is only valid if that assignment has no externally observable effects. `assume` makes the transformation *unconditionally* valid, even when executing 'b=a+1' would affect the output of the program. The compiler can /assume/ that the condition never fails. Hence, it does not need to generate any code to check that the assumption is valid. It does not need to emit any code for any path that would only be taken if the condition would be false. If that ever happens the CPU can start executing any random instructions. That's ok, since you explicitly told the compiler that this situation will never occur. Hence, it can also skip generating any code for any path that unconditionally leads to a failing `assume` directive. Because it is all dead code that will never be executed, as long as all `assume` conditions are true. artur
