August 01, 2010
On 08/01/2010 07:04 AM, bearophile wrote:
> Walter Bright:
>>> /*@ assert (\forall int i; 0<= i&&  i<  n; a[i] != null);
>>
>> This does not make it simpler, it just makes things more
>> complicated by now having two ways to do a foreach.
>
> The point here is to restrict a lot the kind of code and instructions
> you can put inside contracts, so eventually you will have a chance to
> test them automatically.
>
> When you have copied Eiffel to design D contracts you probably have
> seen that in Eiffel you can't put arbitrary code inside contracts
> (the same is true for contract systems in C# and Java, here it's D
> that is designed in the wrong way). This is a limit that was there
> because otherwise it kills the possibility of enforcing them
> statically.

I think D made the right choice here. The space of contracts that can be effectively checked during compilation is very small, and the relative complexity of the checkers is very high. (Array bounds checking is a classic example.) Restricting contracts to make them statically checkable with today's technology would essentially push them out of existence.

Andrei
September 11, 2010
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

1 2 3
Next ›   Last »