A problem with D contracts

[Walter Bright]

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.

Replacing foreach with another looping construct does absolutely nothing to 
enhance analyse-ability. You could replace them with a rat's nest of goto's and 
the compiler can still figure it out using standard, well known algorithms.

dmd's global optimizer is an example of this. In fact, all structured statements 
are reduced to if's and goto's before handing them to the optimizer, and the 
optimizer reconstructs all the loops, etc., from that flow graph. It's 1970's 
technology <g>.


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

No, it doesn't kill it at all. It only kills it for *some* contracts.