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. Bye, bearophile
