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.
