A problem with D contracts

[Norbert Nemec]

I agree that contracts offer too much liberty. However, I would actually 
go one step further than bearophile:

I find the need for "assert" statements not only superfluous but 
actually misleading. A contract violation is something conceptionally 
different from a broken assertion. Assertions and contracts have 
different purposes.

In my opinion, contracts should not be lists of statements but simply 
boolean expressions that have to evaluate to true. Contract checks would 
then become decoupled from assertion checks. Both could be switched 
independently at compile time.

For any case where the contract is more complex than what can be handled 
by an expression, one should simply define a pure function, which would 
even help to unclutter the code and keep contract short and concise to read.

Greetings,
Norbert


On 01/08/10 02:33, bearophile wrote:
> D contract programming lacks the 'old', but there is another different problem.
>
> Allowing only asserts (and calls to only pure/readonly functions) in precoditions, postconditions and invariants opens the door for future software that perform automatic compile-time verification of contracts.
>
> Putting all kind of D code inside contracts will make them very hard to statically verify.
>
> But simple asserts sometimes are not enough to test more complex things. So other more serious contract systems allow for asserts that contain forall, max, min, sets, and few more simple things, this is an example from a system for Java:
>
> /*@ assert (\forall int i; 0<= i&&  i<  n; a[i] != null);
>
> Beside keeping the door open to future automatic verification, that short style for conditions helps keep them shorter and less buggy (also because it helps psychological 'chunking'). If code inside contracts is long and complex then it too can contain bugs.
>
> Bye,
> bearophile