• bearophile (12/12) Apr 27 2010 In a recent post I have asked to complete D Contract Programming with lo...
• Norbert Nemec (9/21) Apr 27 2010 I still do not think that there is a need for loop invariants as an
• Lutger (45/45) Apr 28 2010 What do you think about expressing the loop invariant as as nested pure
• bearophile (8/10) Apr 28 2010 It's good enough to satisfy the basic 'requirements' I have listed for a...

bearophile <bearophileHUGS lycos.com> writes:

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

Norbert Nemec <Norbert Nemec-online.de> writes:

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

Lutger <lutger.blijdestijn gmail.com> writes:

What do you think about expressing the loop invariant as as nested pure 
function?

something like this:

body
{
    Node* p = list_header; // pointer to the current Node
    Node* pp; // pointer to the precedent Node

    pure void checkInvariant(in Node* _pp,
                             in Node* _p,
                             in Node* _list_header,
                             in Node* _nptr)
    {
        // predecessor relation
        assert((_pp == null && _p == _list_header) || (_pp != null && 
_pp.next == _p));

        // predecessor before data
        assert(_pp == null || _pp.data < _nptr.data);

        // current before data
        assert(_p == null || _p.data < _nptr.data); // extra

        // data less than
        // forall k : rowList   row .. pp :: k.column < column
        debug { // slow
            if (_pp != null && _list_header != _pp) {
                assert(_list_header.data < _nptr.data);
                const(Node)* _pk = _list_header.next;
                while (_pk != _pp) {
                    assert(_pk.data < _nptr.data);
                    _pk = _pk.next;
                }
            }
        }
    }

    while (p != null && p.data < nptr.data) {
        checkInvariant(pp,p,list_header,nptr);

        pp = p;
        p = p.next;
    }

    assert((pp == null && p == list_header) || (pp != null && pp.next == p));
    assert(pp == null || pp.data < nptr.data);

    if (pp != null)
        pp.next = nptr;
    else
        list_header = nptr;
    nptr.next = p;
}

bearophile <bearophileHUGS lycos.com> writes:

Lutger:

 What do you think about expressing the loop invariant as as nested pure 
 function?

It's good enough to satisfy the basic 'requirements' I have listed for a
invariant syntax :-)
Thank you for the idea.

That D code that tests the invariant is long. This was part of the invariant in
Eiffel that translated to D requires some lines:
forall k : rowList   row .. pp :: k.column < column

From what I have seen so far contracts are a place where language conciseness
is really important. Because they must be correct, use short space, they are
almost mathematical in their nature. Some of the "micropatterns" Andrei has put
in std.range can help a bit here (to shorten the code inside contracts), I will
probably give more micropatterns to Andrei to add them to std.range. I can't
believe how only few languages like Lisp and Python seem to have understood how
fundamental micropatterns are in programming.

Bye,
bearophile