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
