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.
