A problem with D contracts

[KennyTM~]

On Aug 1, 10 09: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.
>

That's too restrictive. If the goal is to verify statically (verify at 
compile time), then allow all CTFE-able code, not just asserts + pure 
functions.

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

Even if only assert is allowed in the outermost level, I don't see why 
\forall is needed.

    assert(reduce!"a&&b"(map!"a!=null"(a[0..n])))

but both are not simpler than

    foreach (i; 0..n)
      assert(a[i] != null);


(BTW, there should be an 'all = reduce!"a&&b"' and 'any = reduce!"a||b"' 
in std.algorithm, but short-circuited.)

> 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