On Friday, 1 August 2014 at 02:44:51 UTC, Walter Bright wrote:
That entry makes no mention of assert being used as an
optimization hint.
Saying that a predicate is always true means it's available to
the optimizer.
An assert does not say that the predicate is always true. It says
that this is a theorem to be proven true given the assumptions
provided up till that point.
If you:
1. have a set of preconditions (assumptions)
2. and a fully specified postcondition
3. and the code between has no sideeffects
4. and the postcondition has been proven true
Only then can you use the postcondition to eliminate code that
was unneccessary to prove the postcondition from the precondition.
So yes, you CAN use asserts to do heavy duty optimization that go
way beyond what a regular optimizer can do (even in theory), but
not a priori.
In theory you can reduce a general algorithm that does too much
work down to the specifics of the postcondition. Doing this for
an imperative language is not realistic today.
DESIGN BY CONTRACT
Design by contract does not mean that programmers guarantee the
postconditions. Quite the opposite!
Design by contract assumes 3 roles:
1. the trusted ARCHITECT who specifies the modules and
pre/postconditions
2. the distrusted IMPLEMENTORS who write the code and cannot
touch the contract
3. the trusted BUILD SYSTEM who guarantees that the contracts are
upheld between modules, either by proof of run time checks that
takes place before one module get access to another.
Claiming that the programmer guarantee asserts to hold true is
not design by contract.
Claiming that the build system is responsible for upholding the
contract despite programmers doing their utmost to break it is
Design by contract.
