• bearophile (38/38) Apr 22 2014 In most languages (even in D) there are testing tools based

"bearophile" <bearophileHUGS lycos.com> writes:

In most languages (even in D) there are testing tools based 
QuickCheck, that is a important alternative (or an extra tool to 
use) to the normal unittesting:

http://en.wikipedia.org/wiki/QuickCheck

The programmer writes assertions about logical properties that a 
function should fulfill, then QuickCheck tries to falsify those 
assertions generating many "random" inputs for the function.

In a D program you have both normal asserts/exceptions/errors and 
the asserts inside contracts:


int foo(int x)
in {
     assert(x >= 0);
} body {
     assert(x < 10);
     return 0;
}
void main() {
     foo(-2);
}


So is it a good idea to tell them apart with a type, like 
generate a "ContractAssertError" instead of an "AssertError" if 
the assert is fired in the contracts?

I think QuickCheck-like testing tools could enjoy to use the type 
to tell apart errors/exceptions in the code from 
ContractAssertErrors. A ContractAssertError is not an error of 
the function, it means the mistake is elsewhere (like in the the 
specified bounds given to the QuickCheck-like tool, a bug in the 
tool itself, etc).

For this idea to work, if a contract calls a function and that 
function throws an assert, that AssertError should be a 
ContractAssertError instead. To do this I think the contracts 
have to catch the AssertErrors and rethrow them as 
ContractAssertErrors.

(Another problem is that some people throw exceptions from 
pre-conditions when they fail, but we can ignore this, it's not a 
good practice in contract-programming terms.)

Bye,
bearophile