I still do not think that there is a need for loop invariants as an
explicit language feature. Putting an assertion at the beginning of a
loop achieves the same purpose. The difference in clarity is marginal,
in my opinion.
This does not say anything about their use in helping designing a loop.
When writing a loop, it does indeed often make sense to think of an
invariant and put this at the top of the loop as assertion (put the word
"invariant" in a comment next to it if you like...)
On 27/04/10 12:51, bearophile wrote:
In a recent post I have asked to complete D Contract Programming with loop
invariants, similar to Eiffel ones:
http://www.digitalmars.com/webnews/newsgroups.php?art_group=digitalmars.D&article_id=107773
Now I am reading a good book about algorithms that uses loop invariants often.
And then I have just read this nice blog post that shows well why sometimes it
can be quite useful to define loop invariants, here to write a correct binary
search:
http://reprog.wordpress.com/2010/04/25/writing-correct-code-part-1-invariants-binary-search-part-4a/
A syntax for loop invariants is not necessary in D, just as a syntax for
contracts or documentation comments is not necessary, but they help formalize
and enforce a good practice, as I have written in the past post:
- It self-documents its purpose;
- You can't forget to create a new scope, this is a little safer;
- In future it can be enforced to be @readonly (that is, the programmer can be
sure the code inside the invariant can't modify the variables in outside the
scope of the invariant, but can read them);
- There can be only one loop invariant, and it must be before the body of the
loop. This helps better separate the asserts from the body of the loop, and
keeps things tidy.
In practice in my opinion many loops in a D program don't need to contain an
explicit loop invariant, this is true even in Eiffel programs. It's mostly
useful in more complex loops, like when you want to write a binary search. But
the loop invariant syntax I've proposed is light and easy to read, and it's
optional, so I think it doesn't hurt if you don't want to use it in many cases.
But when you want it, it's there (the successive blog post will probably be
about the loop variant, that's useful to be more sure that a loop ends).
Bye,
bearophile
