next up previous contents
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)

Fri May 24 19:01:27 BST 1996