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
}
