Re: Loop invariant for a binary search

[Lutger]

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;
}