examples/snapshotable_trees.mlw

   1
   2 (*
   3 Snapshotable Trees
   4
   5 Formalized Verification of Snapshotable Trees: Separation and Sharing
   6 Hannes Mehnert, Filip Sieczkowski, Lars Birkedal, and Peter Sestoft
   7 VSTTE 2012
   8 *)
   9
  10 (* Purely applicative binary trees with elements at the nodes *)
  11
  12 theory Tree
  13
  14   use export int.Int
  15   use export list.List
  16   use export list.Length
  17   use export list.Append
  18
  19   type elt = int
  20
  21   type tree =
  22     | Empty
  23     | Node tree elt tree
  24
  25   function tree_elements (t: tree) : list elt = match t with
  26     | Empty -> Nil
  27     | Node l x r -> tree_elements l ++ Cons x (tree_elements r)
  28   end
  29
  30   predicate mem (x: elt) (t: tree) = match t with
  31     | Empty -> false
  32     | Node l y r -> mem x l || x = y || mem x r
  33   end
  34
  35 end
  36
  37 (* Purely applicative iterators over binary trees *)
  38
  39 module Enum
  40
  41   use Tree
  42
  43   type enum =
  44     | Done
  45     | Next elt tree enum
  46
  47   function enum_elements (e: enum) : list elt = match e with
  48     | Done -> Nil
  49     | Next x r e -> Cons x (tree_elements r ++ enum_elements e)
  50   end
  51
  52   let rec enum t e variant {t}
  53     ensures { enum_elements result = tree_elements t ++ enum_elements e }
  54   = match t with
  55     | Empty -> e
  56     | Node l x r -> enum l (Next x r e)
  57     end
  58
  59 end
  60
  61 (* Mutable iterators with a Java-like API *)
  62
  63 module Iterator
  64
  65   use Tree
  66   use Enum
  67
  68   type iterator = { mutable it: enum }
  69
  70   function elements (i: iterator) : list elt = enum_elements i.it
  71
  72   let create_iterator (t: tree)
  73     ensures { elements result = tree_elements t }
  74   = { it = enum t Done }
  75
  76   predicate hasNext (i: iterator) = i.it <> Done
  77
  78   let hasNext (i: iterator)
  79     ensures { result = True <-> hasNext i }
  80   = match i.it with Done -> False | _ -> True end
  81
  82   let next (i: iterator)
  83     requires { hasNext i }
  84     ensures { old (elements i) = Cons result (elements i) }
  85   = match i.it with
  86     | Done -> absurd
  87     | Next x r e -> i.it <- enum r e; x
  88     end
  89
  90 end
  91
  92 (* Binary search trees *)
  93
  94 module BSTree
  95
  96   use export Tree
  97
  98   predicate lt_tree (x: elt) (t: tree) =
  99     forall y: elt. mem y t -> y < x
 100
 101   predicate gt_tree (x: elt) (t: tree) =
 102     forall y: elt. mem y t -> x < y
 103
 104   predicate bst (t: tree) =
 105     match t with
 106     | Empty -> true
 107     | Node l x r -> bst l /\ bst r /\ lt_tree x l /\ gt_tree x r
 108     end
 109
 110   let rec bst_mem (x: elt) (t: tree)
 111     requires { bst t } ensures { result=True <-> mem x t } variant { t }
 112   = match t with
 113     | Empty ->
 114         False
 115     | Node l y r ->
 116         if x < y then bst_mem x l else x = y || bst_mem x r
 117     end
 118
 119   exception Already
 120     (* bst_add raises exception Already when the element is already present *)
 121
 122   let rec bst_add (x: elt) (t: tree)
 123     requires { bst t }
 124     ensures { bst result /\ not (mem x t) /\
 125       forall y: elt. mem y result <-> y=x || mem y t }
 126     raises { Already -> mem x t }
 127     variant { t }
 128   = match t with
 129     | Empty ->
 130         Node Empty x Empty
 131     | Node l y r ->
 132         if x = y then raise Already;
 133         if x < y then Node (bst_add x l) y r else Node l y (bst_add x r)
 134     end
 135
 136 end
 137
 138 (* Imperative trees with add/contains/snapshot/iterator API *)
 139
 140 module ITree
 141
 142   use export BSTree
 143   use export Iterator
 144
 145   type itree = { mutable tree: tree } invariant { bst tree }
 146
 147   let create () = { tree = Empty }
 148
 149   let contains (t: itree) (x: elt)
 150     ensures { result=True <-> mem x t.tree }
 151   = bst_mem x t.tree
 152
 153   let add (t: itree) (x: elt)
 154     ensures { (result=False <-> mem x (old t.tree)) /\
 155       forall y: elt. mem y t.tree <-> y=x || mem y (old t.tree) }
 156   = try t.tree <- bst_add x t.tree; True with Already -> False end
 157
 158   let snapshot (t: itree) = { tree = t.tree }
 159
 160   let iterator (t: itree)
 161     ensures { elements result = tree_elements t.tree }
 162   = create_iterator t.tree
 163
 164 end
 165
 166 module Harness
 167
 168   use ITree
 169
 170   let test () =
 171      let t = create () in
 172      let _ = add t 1 in
 173      let _ = add t 2 in
 174      let _ = add t 3 in
 175      assert { mem 2 t.tree };
 176      let s = snapshot t in
 177      let it = iterator s in
 178      while hasNext it do
 179        invariant { bst t.tree }
 180        variant { length (elements it) }
 181        let x = next it in
 182        let _ = add t (x * 3) in
 183        ()
 184      done
 185
 186 end