checkedint call removal

[via Digitalmars-d]

On Thursday, 31 July 2014 at 20:24:09 UTC, Walter Bright wrote:
> Code that relies on assertions being false is semantically 
> broken.

Code transforms that relies on unproven theorems to be true are 
semantically broken.

Assertions are proposed theorems.

Assumptions are preconditions needed for those theorems.

The contract is not fulfilled until the theorems are proven. 
PROVEN, not tested by sampling. Until then programming by 
contract (as defined) requires testing under execution, not only 
in debug builds.

If you don't do this, then don't call it programming by contract!


You should also then require the following:

"supplier B guarantees postcondition of B's methods assuming 
client A guarantees the preconditions of those methods"

http://www.cs.usfca.edu/~parrt/course/601/lectures/programming.by.contract.html

So you need this structure:

A(){
    assert(B_preconditions); // try to optimize these away
    B();
    assume(B_postconditions); // not required, but useful for 
optimization
}

B(){
    assume(B_preconditions)
    …execute…
    assert(B_postconditions) // try to get rid of this through 
formal proof
}