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
