A problem with D contracts

[Jay Byrd]

On Sat, 31 Jul 2010 21:33:09 -0400, bearophile wrote:

> D contract programming lacks the 'old', but there is another different
> problem.

Yet another problem is that the logic is completely wrong. The 
preconditions that should be executed are those of the static type -- the 
contract is with the invoker -- not some disjunction or conjunction of 
conditions of the dynamic type stack. Better examples and explanations in 
TDPL would make this issue clear. The problems with the current 
implementation goes unnoticed because it is way too lenient, silently 
failing to impose requirements and provide guarantees.

-- JB

> 
> 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