examples/verifythis_2016_tree_traversal.mlw

   1
   2 (**
   3
   4 {1 VerifyThis @ ETAPS 2016 competition, Challenge 2: Binary Tree Traversal}
   5
   6 {h
   7
   8 The following is the original description of the verification task,
   9 reproduced verbatim from
  10 <a href="http://http://etaps2016.verifythis.org/challenges">the competition web site</a>
  11
  12 <pre>
  13
  14 Challenge 2: Binary Tree Traversal
  15
  16 Consider a binary tree:
  17
  18   class Tree {
  19     Tree left, right, parent;
  20     bool mark;
  21   }
  22
  23 We are given a binary tree with the following properties:
  24 It is well formed, in the sense that following a child pointer (left or right) and then following a parent pointer brings us to the original node. Moreover, the parent pointer of the root is null.
  25 It has at least one node, and each node has 0 or 2 children.
  26 We do not know the initial value of the mark fields.
  27
  28 Our goal is to set all mark fields to true. The algorithm below (Morris 1979) works in time linear in the number of nodes, as usual, but uses only a constant amount of extra space.
  29
  30   void markTree(Tree root) {
  31     Tree x, y;
  32     x = root;
  33     do {
  34           x.mark = true;
  35           if (x.left == null && x.right == null) {
  36                   y = x.parent;
  37           } else {
  38                 y = x.left;
  39                 x.left = x.right;
  40                 x.right = x.parent;
  41                 x.parent = y;
  42           }
  43           x = y;
  44     } while (x != null);
  45   }
  46
  47 Tasks. Prove that:
  48 upon termination of the algorithm, all mark fields are set
  49 the tree shape does not change
  50 the code does not crash, and
  51 the code terminates.
  52
  53 As a bonus, prove that the nodes are visited in depth-first order
  54 </pre>}
  55
  56 The following is a solution by Martin Clochard (Université Paris-Sud)
  57 who entered the competition.
  58
  59 *)
  60
  61 (** Component-as-array memory model with null pointers. *)
  62 module Memory
  63
  64   use map.Map
  65   (** `loc` is the type of memory locations (e.g pointers) *)
  66   type loc
  67   val predicate eq (x y:loc) ensures { result <-> x = y }
  68   (** Kinds of pointer fields. *)
  69   type kind = Parent | Left | Right
  70   (** Convenience alias for a pointer field table. *)
  71   type pmem = map kind (map loc loc)
  72   type memory = abstract {
  73     mutable accessor : pmem;
  74     mutable mark : map loc bool;
  75   }
  76   (** `memo` represent memory. *)
  77   val memo : memory
  78   (** the memory model has a `null` pointer. *)
  79   constant null : loc
  80   val null () : loc ensures { result = null }
  81   val is_null (l:loc) : bool ensures { result <-> l = null }
  82   (** Memory getter & setters. non-null preconditions to
  83       check absence of null pointer access. *)
  84   val get_mark (l:loc) : bool
  85     requires { l <> null }
  86     reads { memo }
  87     ensures { result = memo.mark[l] }
  88   val set_mark (l:loc) (b:bool) : unit
  89     requires { l <> null }
  90     writes { memo.mark }
  91     ensures { memo.mark = (old memo).mark[l <- b] }
  92   val get_acc (p:kind) (l:loc) : loc
  93     requires { l <> null }
  94     reads { memo }
  95     ensures { result = memo.accessor[p][l] }
  96   val set_acc (p:kind) (l d:loc) : unit
  97     requires { l <> null }
  98     writes { memo.accessor }
  99     ensures { memo.accessor =
 100       (old memo).accessor[p <- (old memo).accessor[p][l <- d]] }
 101   (** Ghost global accessors. Those are technical tools
 102       to create ghost witnesses of past states. *)
 103   val ghost get_all_accs () : pmem
 104     reads { memo }
 105     ensures { result = memo.accessor }
 106   val ghost get_all_marks () : map loc bool
 107     reads { memo }
 108     ensures { result = memo.mark }
 109
 110   (** Non-deterministic initialization. In the original alorithm,
 111       the variable y starts uninitialized. *)
 112   type non_det_magic
 113   type non_det = abstract { mutable non_det_field : non_det_magic }
 114   val non_det : non_det
 115   val anyloc () : loc writes { non_det }
 116
 117 end
 118
 119 (** In module `TreeShape` we describe the correlation between
 120     the memory and the binary tree model. We also gives
 121     elements of the algorithm specification, and prove
 122     some frame/separation properties. *)
 123 module TreeShape
 124
 125   use int.Int
 126   use set.Set
 127   use map.Map
 128   use bintree.Tree
 129   use bintree.Size
 130   use Memory
 131
 132   (** The described structure can be modeled as a tree of locations *)
 133   type treel = tree loc
 134
 135   (** `is_tree memo t c p` describe the fact that `c` points to
 136       a well-formed tree modeled by `t`, whose root parent node is `p`.  *)
 137   predicate is_tree (memo:pmem) (t:treel) (c p:loc) = match t with
 138     | Empty -> c = null
 139     | Node l m r -> c <> null /\ c = m /\ memo[Parent][c] = p /\
 140       let cl = memo[Left][c] in
 141       let cr = memo[Right][c] in
 142       (cl = null <-> cr = null) /\
 143       is_tree memo l cl c /\ is_tree memo r cr c
 144     end
 145
 146   (** `footprint t` is the memory footprint of `t`, e.g the set of
 147       locations occuring in the tree. *)
 148   function footprint (t:treel) : set loc = match t with
 149     | Empty -> empty
 150     | Node l m r -> add m (union (footprint l) (footprint r))
 151     end
 152
 153   (** `ext s memo1 memo2` mean that the pointer fields associated to
 154       locations in set `s` are identical in memo1 and memo2. *)
 155   predicate ext (s:set loc) (memo1 memo2:pmem) =
 156     forall k x. mem x s -> memo1[k][x] = memo2[k][x]
 157   (** `unchanged memo1 memo2` mean that all pointer fields in
 158       `memo1` and `memo2` are identical. *)
 159   predicate unchanged (memo1 memo2:pmem) =
 160     forall k x. memo1[k][x] = memo2[k][x]
 161   (** `was_marked t memo1 memo2` mean that `memo2` is the update
 162       of `memo1` obtained by marking all elements in `t`. *)
 163   predicate was_marked (t:treel) (memo1 memo2:map loc bool) =
 164     (forall l. mem l (footprint t) -> memo2[l]) /\
 165     (forall l. not mem l (footprint t) -> memo2[l] = memo1[l])
 166
 167   (** General extensionality property. *)
 168   let rec ghost ext_set (s:set loc) (memo1 memo2:pmem)
 169                                     (t:treel) (c p:loc) : unit
 170     requires { ext s memo1 memo2 }
 171     requires { subset (footprint t) s }
 172     requires { is_tree memo1 t c p }
 173     ensures { is_tree memo2 t c p }
 174     variant { t }
 175   = let ghost rc = ext_set s memo1 memo2 in
 176     match t with
 177     | Empty -> ()
 178     | Node l _ r -> rc l (memo1[Left][c]) c; rc r (memo1[Right][c]) c
 179     end
 180
 181   (** Specialized for our use case. *)
 182   let ghost ext_cur (memo1:pmem) (t:treel) (c p:loc) : unit
 183     reads { memo }
 184     requires { ext (footprint t) memo1 memo.accessor }
 185     requires { is_tree memo1 t c p }
 186     ensures { is_tree memo.accessor t c p }
 187   = ext_set (footprint t) memo1 (get_all_accs ()) t c p
 188
 189   (** The tree model corresponding to a given pointer is unique. *)
 190   let rec ghost unicity (memo:pmem) (t1 t2:treel) (c p1 p2:loc) : unit
 191     requires { is_tree memo t1 c p1 /\ is_tree memo t2 c p2 }
 192     ensures { t1 = t2 }
 193     variant { t1 }
 194   = match t1, t2 with
 195     | Empty, Empty -> ()
 196     | Empty, _ | _, Empty -> absurd
 197     | Node l1 _ r1, Node l2 _ r2 ->
 198         unicity memo l1 l2 (memo[Left][c]) c c;
 199         unicity memo r1 r2 (memo[Right][c]) c c
 200     end
 201
 202   (** In a non-empty well formed tree, the top pointer
 203       cannot occur in the child subtree. Otherwise,
 204       their would be an infinite branch in the tree,
 205       which is impossible in our inductive tree setting. *)
 206   let ghost not_below (memo:pmem) (lf rg:treel) (c p:loc) : unit
 207     requires { is_tree memo (Node lf c rg) c p }
 208     ensures { not mem c (footprint lf) /\ not mem c (footprint rg) }
 209   = let t0 = Node lf c rg in
 210     let rec aux (t:treel) (c2 p2:loc) : unit
 211       requires { size t < size t0 }
 212       requires { is_tree memo t c2 p2 }
 213       ensures { not mem c (footprint t) }
 214       variant { t }
 215     = match t with
 216       | Empty -> ()
 217       | Node l _ r ->
 218         if eq c2 c then (unicity memo t t0 c p2 p;absurd);
 219         aux l (memo[Left][c2]) c2; aux r (memo[Right][c2]) c2
 220       end in
 221     aux lf (memo[Left][c]) c; aux rg (memo[Right][c]) c
 222
 223   (** Algorithm phases.
 224       `GoLeft` mean that the algorithm will try to explore the left
 225         subtree
 226       `GoRight` mean that the algorithm will explore the right subtree
 227       `GoBack` mean that the algorithm will go back to the parent node
 228       `Finish` mean that the alogrithm will exit *)
 229   type phase =
 230     | GoLeft
 231     | GoRight
 232     | GoBack
 233     | Finish
 234
 235   function next_phase (ph:phase) : phase =
 236     match ph with
 237     | GoLeft -> GoRight
 238     | GoRight -> GoBack
 239     | GoBack -> GoLeft
 240     | Finish -> Finish
 241     end
 242   (** `rotated memo1 memo2 ph c` describe how `c` is rotated in
 243       `memo2` with respect to its initial position in `memo1` for
 244       current phase `ph`. In final phase, it is not rotated but
 245       null instead. *)
 246   predicate rotated (memo1 memo2:pmem) (ph:phase) (c:loc) =
 247     (forall k x. x <> c -> memo1[k][x] = memo2[k][x]) /\
 248     (ph <> Finish -> c <> null) /\
 249     match ph with
 250     | GoLeft -> unchanged memo1 memo2
 251     | GoRight -> memo2[Left][c] = memo1[Right][c] /\
 252         memo2[Right][c] = memo1[Parent][c] /\
 253         memo2[Parent][c] = memo1[Left][c]
 254     | GoBack -> memo1[Left][c] = memo2[Right][c] /\
 255         memo1[Right][c] = memo2[Parent][c] /\
 256         memo1[Parent][c] = memo2[Left][c]
 257     | Finish -> c = null
 258     end
 259
 260 end
 261
 262 (** In this module, we prove the algorithm by modifying
 263     the code to put it in recursive form. We justify that
 264     our limited usage of recursion makes the code equivalent
 265     to the one proposed in the challenge. *)
 266 module Recursive
 267
 268   use map.Map
 269   use bintree.Tree
 270   use ref.Ref
 271   use Memory
 272   use TreeShape
 273
 274   (** Recursion-based proof of the algorithm.
 275       The principal idea is the following: in its recursive
 276       fashion, the algorithm is a standard tree traversal
 277       (which is easy to prove correct).
 278       Hence we nest the algorithm inside a recursive procedure
 279       to link it with its recursive version. However,
 280       the obtained algorithm does not really need the call stack
 281       to run. Here is how we achieve this:
 282       - We create a non-recursive sub-routine `bloc` corresponding to
 283         one turn of the while loop in the challenge's code.
 284         It uses an exception to simulate exit.
 285         Also, this sub-routine does not have any non-ghost argument,
 286         so calling `bloc` really amounts to advancing in the loop execution.
 287       - We forbids use of any side-effect in the recursive procedure
 288         except those obtained by calling `bloc`. Hence calling
 289         the recursive procedure is equivalent to run a certain
 290         amounts of turns in the loop execution.
 291         Note that since we will prove that the recursive procedure
 292         terminates, it might not run a finite amount of turns and diverges
 293         afterward.
 294       - After the topmost call to the recursive procedure,
 295         we add an infinite loop who only calls `bloc` at every turns.
 296         This call and the loop are enclosed in an exception catching
 297         construction to detect loop termination.
 298       Hence it is justifiable that the algorithm with
 299       the recursive procedure is equivalent (in the sense that
 300       they have the same side-effects) as an infinite loop of `bloc` calls,
 301       encapsulated in an exception catching expression. And this
 302       algorithm is evidently equivalent to the original challenge code.
 303     *)
 304
 305   exception Stop
 306
 307   let markTree (ghost t:treel) (root:loc) : unit
 308     (* Requires a well-formed non-empty tree *)
 309     requires { is_tree memo.accessor t root null /\ root <> null }
 310     writes { memo, non_det }
 311     (* Tree shape is unchanged *)
 312     ensures { is_tree memo.accessor t root null }
 313     ensures { unchanged (old memo).accessor memo.accessor }
 314     (* All nodes are marked. *)
 315     ensures { was_marked t (old memo).mark memo.mark }
 316   = let x = ref (anyloc ()) in (* ==> Tree x, y *)
 317     let y = ref (anyloc ()) in
 318     x := root; (* ==> x = root *)
 319     let entered = ref false in
 320     (* ^ Used to encode the do { .. } while() loop as a while() {..}.
 321        Iterations will set the flag. *)
 322     let ghost z = ref (null ()) in (* Store previously explored node. *)
 323     (* Loop body. `mem0` is memory state at start of recursive call,
 324        `ph` is phase. *)
 325     let bloc (ghost mem0:pmem) (ghost ph:phase) : unit
 326       (* current node `!x` is rotated correctly with
 327          respect to the phase. *)
 328       requires { rotated mem0 memo.accessor ph !x }
 329       requires { ph = Finish -> !entered }
 330       writes { memo, x, y, z, entered }
 331       (* Caracterise `x` and `z` reference updates. *)
 332       ensures { !z = !(old x) /\ !x = memo.accessor[Parent][!z] }
 333       (* `Finish` phase never ends normally *)
 334       ensures { ph <> Finish /\ !entered }
 335       (* Node is marked, and other nodes do not change. *)
 336       ensures { memo.mark[!z] }
 337       ensures { forall l. l <> !z -> memo.mark[l] = (old memo).mark[l] }
 338       (* Describe phase shift. *)
 339       ensures {
 340         if (old memo).accessor[Left][!z] = null
 341            = (old memo).accessor[Right][!z]
 342         then memo.accessor = (old memo).accessor
 343         else rotated mem0 memo.accessor (next_phase ph) !z }
 344       (* In `Finish` phase, the code throws `Stop` without changing
 345          anything. *)
 346       raises { Stop -> ph = Finish /\ memo = old memo }
 347     = if !entered && is_null !x then raise Stop; (* ==> do { BODY         *)
 348       entered := true;                           (*  } while (x != null); *)
 349       (ghost z := !x);
 350       set_mark !x true; (* ==> x.mark = true; *)
 351       if is_null (get_acc Left !x) && is_null (get_acc Right !x)
 352          (* ==> if (x.left = null && x.right == null) { *)
 353       then y := get_acc Parent !x (* ==> y = x.parent *)
 354       else begin (* ==> } else { *)
 355         y := get_acc Left !x; (* ==> y = x.left; *)
 356         set_acc Left !x (get_acc Right !x); (* ==> x.left = x.right; *)
 357         set_acc Right !x (get_acc Parent !x); (* ==> x.right = x.parent; *)
 358         set_acc Parent !x !y; (* ==> x.parent = y; *)
 359       end; (* ==> } *)
 360       x := !y (* ==> x = y; *)
 361     in
 362     (* 'Recursive proof', corresponding to the
 363         expected depth-first traversal. *)
 364     let rec aux (ghost t:treel) : unit
 365       requires { !x <> null }
 366       requires { is_tree memo.accessor t !x !z }
 367       writes { memo, x, y, z, entered }
 368       ensures { unchanged (old memo).accessor memo.accessor }
 369       ensures { !x = old !z /\ !z = old !x }
 370       ensures { was_marked t (old memo).mark memo.mark }
 371       ensures { !entered }
 372       raises { Stop -> false }
 373       variant { t }
 374     = let ghost mem0 = get_all_accs () in
 375       let ghost _c = !x in
 376       let _lf = get_acc Left !x in
 377       let _rg = get_acc Right !x in
 378       let lf, rg = ghost match t with
 379         | Empty -> absurd
 380         | Node l _ r -> l, r
 381         end in
 382       (ghost not_below mem0 lf rg _c !z);
 383       bloc mem0 GoLeft;
 384       let b = begin ensures { result <-> _lf = null /\ _rg = null }
 385         ensures { result -> lf = Empty /\ rg = Empty }
 386         is_null _lf && is_null _rg end in
 387       if not b then begin
 388         (ghost ext_cur mem0 lf _lf _c);
 389         aux lf;
 390         bloc mem0 GoRight;
 391         (ghost ext_cur mem0 rg _rg _c);
 392         aux rg;
 393         bloc mem0 GoBack
 394       end
 395     in
 396     let ghost mem0 = get_all_accs () in
 397     try aux t;
 398       label I in
 399       while true do
 400         invariant { memo = (memo at I) }
 401         invariant { rotated mem0 memo.accessor Finish !x /\ !entered }
 402         variant { 0 }
 403         bloc mem0 Finish
 404       done
 405     with Stop -> (ghost ext_cur mem0 t root (null ())); () end
 406
 407 end
 408
 409 (** In this module we provide a proof of the initial algorithm by
 410     derecursiving the previous one *)
 411 module Iterative
 412
 413   use int.Int
 414   use map.Map
 415   use map.Const
 416   use bintree.Tree
 417   use bintree.Size
 418   use option.Option
 419   use ref.Ref
 420   use Memory
 421   use TreeShape
 422
 423   (** Snapshot of all relevant memory values in the program *)
 424   type snap = {
 425     pointers : pmem;
 426     cursor : loc;
 427     parent : loc;
 428     marks : map loc bool;
 429   }
 430
 431   (** Stack frame in the recursive version. Fields are
 432       assigned as the code pointer increase. *)
 433   type frame = {
 434     (* Memory & ghost argument at call site (pc>=0). *)
 435     memo0 : snap;
 436     tree : treel;
 437     (* right & left trees/pointers (pc>=1) *)
 438     tleft : treel;
 439     pleft : loc;
 440     tright : treel;
 441     pright : loc;
 442     (* Memory after first bloc call (pc>=2) *)
 443     memo1 : snap;
 444     (* Memory after first recursive call (pc >= 4) *)
 445     memo2 : snap;
 446     (* Memory after second bloc call (pc >= 5) *)
 447     memo3 : snap;
 448     (* Memory after second recursive call (pc >= 6) *)
 449     memo4 : snap;
 450   }
 451
 452   (** Find out current memory state with respect to code pointer. *)
 453   function frame_memo (f:frame) (pc:int) : snap =
 454     if pc <= 0 then f.memo0
 455     else if pc <= 1 then f.memo1
 456     else if pc <= 2 then f.memo2
 457     else if pc <= 3 then f.memo3
 458     else f.memo4
 459
 460   (** Postcondition relation for `bloc` calls. *)
 461   predicate bloc_rel (mem0:pmem) (ph:phase) (s1 s2:snap) =
 462     s2.parent = s1.cursor /\ s2.cursor = s2.pointers[Parent][s2.parent] /\
 463     s2.marks[s2.parent] /\
 464     (forall l. l <> s2.parent -> s2.marks[l] = s1.marks[l]) /\
 465     if s1.pointers[Left][s1.cursor] = null = s1.pointers[Right][s1.cursor]
 466     then s2.pointers = s1.pointers
 467     else rotated mem0 s2.pointers (next_phase ph) s2.parent
 468
 469   (** postcondition relation for recursive (`aux`) calls. *)
 470   predicate rec_rel (t:treel) (s1 s2:snap) =
 471     unchanged s1.pointers s2.pointers /\
 472     s2.cursor = s1.parent /\ s2.parent = s1.cursor /\
 473     was_marked t s1.marks s2.marks
 474
 475   (** Call stack *)
 476   type stack =
 477     | Bottom
 478     | Running stack int frame
 479     | Done
 480
 481   (** Describe a valid call stack. Mostly precise which relation
 482       between states holds. Note that in the previous version,
 483       Why3 did that part for us via the weakest precondition calculus. *)
 484   predicate is_stack (t:treel) (stop scur:snap)
 485                      (s:stack) (calls:option treel) =
 486     match s with
 487     | Bottom -> stop = scur /\ calls = Some t
 488     | Running s pc f ->
 489         0 <= pc <= 4 /\
 490         (* Correctness of caller stack. *)
 491         let m0 = f.memo0 in
 492         is_stack t stop m0 s (Some f.tree) /\
 493         (* Precondition for recursive call. *)
 494         m0.cursor <> null /\ is_tree m0.pointers f.tree m0.cursor m0.parent /\
 495         (* Initially obtained pointers & subtrees. *)
 496         f.tree = Node f.tleft m0.cursor f.tright /\
 497         f.pleft = m0.pointers[Left][m0.cursor] /\
 498         f.pright = m0.pointers[Right][m0.cursor] /\
 499         (* First bloc run, if completed normally. *)
 500         (pc >= 1 -> bloc_rel m0.pointers GoLeft m0 f.memo1 /\
 501                     f.pleft <> null /\ f.pright <> null) /\
 502         (* First recursive call. *)
 503         (pc >= 2 -> rec_rel f.tleft f.memo1 f.memo2) /\
 504         (* Second bloc run. *)
 505         (pc >= 3 -> bloc_rel m0.pointers GoRight f.memo2 f.memo3) /\
 506         (* Second recursive call. *)
 507         (pc >= 4 -> rec_rel f.tright f.memo3 f.memo4) /\
 508         (* Current memory state. *)
 509         frame_memo f pc = scur /\
 510         match calls with
 511         | None -> pc <> 1 /\ pc <> 3
 512         | Some u ->
 513             if pc = 1 then u = f.tleft else pc = 3 /\ u = f.tright
 514         end
 515     | Done -> rec_rel t stop scur /\ calls = None
 516     end
 517
 518   (** Termination argument. In fully general cases, we would need
 519      a lexicographic ordering but here an integer size suffice. *)
 520   constant large_enough : int = 100
 521   function stack_size (st:stack) : int = match st with
 522     | Bottom -> 1
 523     | Done -> 0
 524     | Running s pc f ->
 525         stack_size s + (large_enough - pc) + if pc = 0
 526         then large_enough * (size f.tleft + size f.tright)
 527         else if pc <= 2
 528         then large_enough * size f.tright
 529         else 0
 530     end
 531
 532   let rec lemma stack_size_pos (st:stack) : unit
 533     requires { exists t stop scur calls. is_stack t stop scur st calls }
 534     ensures { stack_size st >= 0 }
 535     variant { st }
 536   = match st with Running s _ _ -> stack_size_pos s | _ -> () end
 537
 538   (** Create a stack frame for a recursive call *)
 539   let ghost opening (t ct:treel) (stop scur:snap) (ghost st:ref stack)
 540     requires { is_stack t stop scur !st (Some ct) }
 541     requires { is_tree scur.pointers ct scur.cursor scur.parent }
 542     requires { scur.cursor <> null }
 543     writes { st }
 544     ensures { is_stack t stop scur !st None }
 545     ensures { stack_size !st <= stack_size !(old st) +
 546                                 large_enough * size ct }
 547   = match ct with
 548     | Empty -> absurd
 549     | Node lf _ rg ->
 550       let f = {
 551         memo0 = scur; tree = ct; tleft = lf; tright = rg;
 552         pleft = scur.pointers[Left][scur.cursor];
 553         pright = scur.pointers[Right][scur.cursor];
 554         memo1 = scur; memo2 = scur; memo3 = scur; memo4 = scur;
 555       } in
 556       st := Running !st 0 f
 557     end
 558
 559   (** Remove a stack frame at end of recursive call simulation *)
 560   let ghost closing (t ct:treel) (stop sprev scur:snap)
 561                     (ghost st:ref stack) : unit
 562     requires { is_stack t stop sprev !st (Some ct) }
 563     requires { rec_rel ct sprev scur }
 564     writes { st }
 565     ensures { is_stack t stop scur !st None }
 566     ensures { stack_size !st < stack_size !(old st) }
 567   = match !st with
 568     | Bottom -> st := Done
 569     | Done -> absurd
 570     | Running s pc f ->
 571       let f = if pc = 1 then { f with memo2 = scur }
 572       else { f with memo4 = scur } in
 573       st := Running s (pc+1) f
 574     end
 575
 576   (** Advance code pointer when a bloc is run. Takes care to
 577       open/close new frame as needed. *)
 578   let ghost continuing (t:treel) (stop sprev scur:snap)
 579                        (ghost st:ref stack)
 580     requires { is_stack t stop sprev !st None }
 581     requires { match !st with
 582       | Bottom | Done -> false
 583       | Running _ pc f ->
 584           let ph =
 585             if pc = 0 then GoLeft else if pc = 2 then GoRight else GoBack in
 586           bloc_rel f.memo0.pointers ph sprev scur
 587       end }
 588     writes { st }
 589     ensures { is_stack t stop scur !st None }
 590     ensures { stack_size !st < stack_size !(old st) }
 591   = match !st with
 592     | Bottom | Done -> absurd
 593     | Running s pc f ->
 594       not_below f.memo0.pointers f.tleft f.tright
 595                 f.memo0.cursor f.memo0.parent;
 596       if pc = 0 then
 597         if is_null f.pleft && is_null f.pright
 598         then begin
 599           st := s;
 600           assert { match f.tleft, f.tright with
 601             Empty, Empty  -> true | _ -> false end };
 602           closing t f.tree stop f.memo0 scur st
 603         end else begin
 604           let f = { f with memo1 = scur } in
 605           st := Running s (pc+1) f;
 606           ext_set (footprint f.tleft) f.memo0.pointers scur.pointers
 607                   f.tleft f.pleft f.memo0.cursor;
 608           opening t f.tleft stop scur st;
 609         end
 610       else if pc = 2 then begin
 611         let f = { f with memo3 = scur } in
 612         st := Running s (pc+1) f;
 613         ext_set (footprint f.tright) f.memo0.pointers scur.pointers
 614                 f.tright f.pright f.memo0.cursor;
 615         opening t f.tright stop scur st;
 616       end else if pc = 4 then begin
 617         st := s;
 618         assert { unchanged scur.pointers f.memo0.pointers };
 619         closing t f.tree stop f.memo0 scur st
 620       end
 621     end
 622
 623   (** The main algorithm. *)
 624   let markTree (ghost t:treel) (root:loc) : unit
 625     (* Requires a well-formed non-empty tree *)
 626     requires { is_tree memo.accessor t root null /\ root <> null }
 627     writes { memo, non_det }
 628     (* Tree shape is unchanged *)
 629     ensures { is_tree memo.accessor t root null }
 630     ensures { unchanged (old memo).accessor memo.accessor }
 631     (* All nodes are marked. *)
 632     ensures { was_marked t (old memo).mark memo.mark }
 633   = let x = ref (anyloc ()) in (* ==> Tree x, y *)
 634     let y = ref (anyloc ()) in
 635     let ghost z = ref (null ()) in
 636     let ghost snapshot () : snap
 637       ensures { result.pointers = memo.accessor }
 638       ensures { result.cursor = !x }
 639       ensures { result.parent = !z }
 640       ensures { result.marks = memo.mark }
 641     = { pointers = get_all_accs ();
 642         cursor = !x; parent = !z;
 643         marks = get_all_marks () } in
 644     x := root; (* ==> x = root; *)
 645     let ghost stop = snapshot () in
 646     let ghost scur = ref stop in
 647     let ghost st = ref Bottom in
 648     ghost opening t t stop stop st;
 649     let entered = ref false in (* encode do-while loop. *)
 650     while not (begin ensures { result <-> !x = null }
 651         !entered && is_null !x end)
 652     do (* ==> do { BODY } while(x != null); *)
 653       invariant { !x = null -> !entered }
 654       invariant { !scur.pointers = memo.accessor }
 655       invariant { !scur.cursor = !x }
 656       invariant { !scur.parent = !z }
 657       invariant { !scur.marks = memo.mark }
 658       invariant { is_stack t stop !scur !st None }
 659       variant { stack_size !st }
 660       entered := true;
 661       (ghost z := !x);
 662       set_mark !x true; (* ==> x.mark = true; *)
 663       if is_null (get_acc Left !x) && is_null (get_acc Right !x)
 664         (* ==> if (x.left == null && x.right == null) { *)
 665       then begin
 666         y := get_acc Parent !x; (* ==> y = x.parent; *)
 667       end
 668       else begin (* ==> } else { *)
 669         y := get_acc Left !x; (* ==> y = x.left; *)
 670         set_acc Left !x (get_acc Right !x); (* ==> x.left = x.right; *)
 671         set_acc Right !x (get_acc Parent !x); (* ==> x.right = x.parent; *)
 672         set_acc Parent !x !y; (* ==> x.parent = y; *)
 673       end; (* ==> } *)
 674       x := !y; (* ==> x = y; *)
 675       let ghost sprev = !scur in
 676       ghost scur := snapshot ();
 677       ghost continuing t stop sprev !scur st;
 678     done; (* ==> end 'do while' *)
 679     ghost (match !st with Done -> () | _ -> absurd end);
 680     ghost ext_cur stop.pointers t root (null ())
 681
 682 end