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 x is less than y, and y is not bigger than n.
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)