examples/dfs.mlw

   1
   2 (* Depth-First Search
   3    (following François Pottier's lecture INF431 at École Polytechnique)
   4
   5    We are given memory cells with two (possibly null) [left] and [right]
   6    neighbours and a mutable Boolean attribute [marked]. In Java, it would
   7    look like
   8
   9      class Cell { Cell left, right; boolean marked; ... }
  10
  11    We mark all cells that are reachable from a given cell [root] using
  12    depth-first search, that is using the following recursive function:
  13
  14      static void dfs(Cell c) {
  15        if (c != null && !c.marked) {
  16          c.marked = true;
  17          dfs(c.left);
  18          dfs(c.right);
  19        }
  20     }
  21
  22   We wish to prove that, assuming that all cells are initially unmarked,
  23   a call to dfs(root) will mark all cells reachable from root, and only
  24   those cells.
  25
  26 *)
  27
  28 module DFS
  29
  30   use bool.Bool
  31   use map.Map
  32   use ref.Ref
  33
  34   type loc
  35   val constant null: loc
  36   val constant root: loc
  37
  38   val (==) (x y: loc) : bool
  39     ensures { result <-> x = y }
  40
  41   val function left  loc: loc
  42   val function right loc: loc
  43
  44   type marks = map loc bool
  45   val marked: ref marks
  46   val ghost busy: ref marks
  47
  48   let set (m: ref marks) (l: loc) (b: bool) : unit
  49     writes  { m }
  50     ensures { !m = (old !m)[l <- b] }
  51   = let f = !m in
  52     m := fun x -> if x == l then b else f x
  53
  54   predicate edge (x y: loc) = x <> null && (left x = y || right x = y)
  55
  56   inductive path (x y: loc) =
  57   | path_nil: forall x: loc. path x x
  58   | path_cons: forall x y z: loc. path x y -> edge y z -> path x z
  59
  60   predicate only_descendants_are_marked (marked: marks) =
  61     forall x: loc. x <> null && marked[x] = True -> path root x
  62
  63   predicate well_colored (marked busy: marks) =
  64     forall x y: loc. edge x y -> y <> null ->
  65     busy[x] = True || (marked[x] = True -> marked[y] = True)
  66
  67   let rec dfs (c: loc) : unit
  68     requires { well_colored !marked !busy }
  69     requires { only_descendants_are_marked !marked }
  70     requires { path root c }
  71     diverges
  72     ensures  { well_colored !marked !busy }
  73     ensures  { forall x: loc. (old !marked)[x] = True -> !marked[x] = True }
  74     ensures  { c <> null -> !marked[c] = True }
  75     ensures  { forall x: loc. !busy[x] = True -> (old !busy)[x] = True }
  76     ensures  { only_descendants_are_marked !marked }
  77   =
  78     if not (c == null) && not !marked[c] then begin
  79       ghost set busy c True;
  80       set marked c True;
  81       dfs (left c);
  82       dfs (right c);
  83       set busy c False
  84     end
  85
  86   predicate all_descendants_are_marked (marked: marks) =
  87     root <> null ->
  88     marked[root] = True &&
  89     forall x y: loc.
  90       edge x y -> marked[x] = True -> y <> null -> marked[y] = True
  91
  92   lemma reformulation:
  93     forall marked: marks.
  94     all_descendants_are_marked marked ->
  95     forall x: loc. x <> null -> path root x -> marked[x] = True /\ root <> null
  96
  97   let traverse () : unit
  98     requires { forall x: loc. x <> null ->
  99                !marked[x] = False && !busy[x] = False }
 100     diverges
 101     ensures  { only_descendants_are_marked !marked }
 102     ensures  { all_descendants_are_marked !marked }
 103     ensures  { forall x: loc. x <> null -> !busy[x] = False }
 104   =
 105     assert { well_colored !marked !busy };
 106     dfs root
 107
 108 end