checkedint call removal

via Digitalmars-d digitalmars-d at puremagic.com
Wed Jul 30 12:25:39 PDT 2014


On Wednesday, 30 July 2014 at 18:48:21 UTC, H. S. Teoh via 
Digitalmars-d wrote:
> 1) When compiling in non-release mode:
> 	assert(...) means "I believe condition X holds, if it doesn't I
> 		screwed up big time, my program should abort"

Assert(X) means, the specification requires theorem X to be 
proved by all implicit or explicit axioms/assumptions made prior 
to this either implicitly or explicitly.

> 	assume(...) means as "I believe condition X holds, if it 
> doesn't
> 		I screwed up big time, my program should abort"

Assume(X) means, the specification specifies (axiom) X (to hold).

> 2) When compiling in release/optimized mode:
> 	assert(...) means "Trust me, I've made sure condition X holds,
> 		please optimize my code by not bothering to check
> 		condition X again"

No. Assert(X) does not change any meaning. You just turned off 
program verification. Assumes and asserts are annotations.

> 	assume(...) means "Trust me, I've made sure condition X holds,
> 		please optimize my code by making use of condition X"

Assume(X) means that the specification defines X to hold at this 
point.

> in (2), but I don't see the incompatibility. In both cases 
> under (2) we
> are *assuming*, without proof or check, that X holds, and based 
> on that
> we are making some optimizations of the generated code.

Not really. Most of the assumes are implicit in the code. What 
you specify with assume are just additional axioms required by 
the specification in order to prove the assertions. (e.g. the 
ones not embedded implicitly in the code).

> I can't think of a real-life scenario where you'd want to 
> distinguish
> between the two kinds of optimizations in (2).

The difference is that "assume(X)" (or require) are the specified 
preconditions. It does not make the program incorrect per 
definition. However you don't want your program littered with 
preconditions.

So yes, you CAN optimize based on assume() since those are 
restrictions the environment put on the input. But you only have 
a few of those.


More information about the Digitalmars-d mailing list