Next: Pure Martin Löf type Up: Example Previous: The marker phase of

### The correctness proof

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)```

Lego
Fri May 24 19:01:27 BST 1996