Loop invariant for a binary search

Norbert Nemec Norbert at Nemec-online.de
Tue Apr 27 09:52:13 PDT 2010


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




More information about the Digitalmars-d mailing list