We say that a link is `OK` if it is not linking a black node to a white
node.
The predicate `lt_n x y` says that

To propagate the colouring the memory is scanned according to a
bounded version `lt_pair`

of the usual lexicographic order on
pairs.

The predicate `OK_upto`

expresses the fact that the pairs
already scanned are `OK`.

At every stage during the scanning of the memory either a black to
white link was found and the flag `changed` was set to `
true` or all links were `OK`.

The idea of the marking phase is that the collector keeps scanning the
memory until every link is `OK`, in other words, while `changed` is `
true` the collector keeps propagating the colouring.

The invariant of such while loop says that every link is `OK` or there
has been a change. From the definition of `lt_pair`

it follows
that every pair (*i*,*j*) is less than (*n*,0). Then we can express our
invariant as `CHOK` *n* 0.

** Module verify Imports lib_hoare lib_nat_rels mark Ok = ... : (nat->nat->bool)->(nat->bool)->nat->nat->Prop lt_n = ... : nat->nat->Prop lt_pair = ... : (nat#nat)->(nat#nat)->Prop OK_upto = ... : (nat->nat->bool)->(nat->bool)->nat->nat->Prop CHOK = ... : (nat->nat->bool)->(nat->bool)->bool->nat->nat->Prop iSigma : E mark_phase = ... : HD ([_:E]trueProp) mark ([sigma:E]CHOK is_linked (sigma a) (sigma changed) n zero)

Fri May 24 19:01:27 BST 1996