Loop invariant for a binary search
Lutger
lutger.blijdestijn at gmail.com
Wed Apr 28 12:54:38 PDT 2010
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;
}
More information about the Digitalmars-d
mailing list