examples/verifythis_fm2012_treedel.mlw

   1
   2 (** {1 The VerifyThis competition at FM2012: Problem 3}
   3
   4    See {h <a href="http://fm2012.verifythis.org/challenges">this web page</a>}
   5
   6    Author: Jean-Christophe Filliâtre *)
   7
   8 (*
   9 Iterative deletion in a binary search tree - 90 minutes
  10
  11
  12 VERIFICATION TASK
  13 -----------------
  14
  15 Given: a pointer t to the root of a non-empty binary search tree (not
  16 necessarily balanced). Verify that the following procedure removes the
  17 node with the minimal key from the tree. After removal, the data
  18 structure should again be a binary search tree.
  19
  20
  21 (Tree, int) search_tree_delete_min (Tree t) {
  22    Tree tt, pp, p;
  23    int m;
  24    p = t->left;
  25    if (p == NULL) {
  26        m = t->data; tt = t->right; dispose (t); t = tt;
  27    } else {
  28        pp = t; tt = p->left;
  29        while (tt != NULL) {
  30            pp = p; p = tt; tt = p->left;
  31        }
  32        m = p->data; tt = p->right; dispose(p); pp->left= tt;
  33    }
  34    return (t,m);
  35 }
  36
  37 Note: When implementing in a garbage-collected language, the call to
  38 dispose() is superfluous.
  39 *)
  40
  41 (* Why3 has no pointer data structures, so we model the heap *)
  42 module Memory
  43
  44   use export map.Map
  45   use export ref.Ref
  46
  47   type loc
  48   val constant null: loc
  49   val predicate eq_loc (x y:loc)
  50     ensures { result <-> x = y }
  51
  52   type node = { left: loc; right: loc; data: int; }
  53   type memory = map loc node
  54
  55   (* the global variable mem contains the current state of the memory *)
  56   val mem: ref memory
  57
  58   (* accessor functions to ensure safety i.e. no null loc dereference *)
  59   let get_left (p: loc) : loc =
  60     requires { p <> null }
  61     ensures  { result = !mem[p].left }
  62     !mem[p].left
  63   let get_right (p: loc) : loc =
  64     requires { p <> null }
  65     ensures  { result = !mem[p].right }
  66     !mem[p].right
  67   let get_data (p: loc) : int =
  68     requires { p <> null }
  69     ensures  { result = !mem[p].data }
  70     !mem[p].data
  71
  72   val set_left (p: loc) (v:loc) : unit
  73     requires { p <> null }
  74     writes { mem }
  75     ensures  { !mem[p] = { (old !mem)[p] with left = v } }
  76     ensures  { forall q. q <> p -> !mem[q] = (old !mem)[q] }
  77 (* FIXME: This expression makes a ghost modification in the non-ghost variable mem
  78
  79   = mem := set !mem p { !mem[p] with left = v }
  80 *)
  81
  82 end
  83
  84 module Treedel
  85
  86   use Memory
  87   use bintree.Tree
  88   use bintree.Inorder
  89   use list.List
  90   use list.Mem
  91   use list.Append
  92   use list.Distinct
  93
  94   function root (t: tree loc) : loc =
  95     match t with
  96     | Empty -> null
  97     | Node _ p _ -> p
  98     end
  99
 100   (* there is a binary tree t in memory m *)
 101   predicate istree (m: memory) (t: tree loc) =
 102     match t with
 103     | Empty -> true
 104     | Node l p r -> p <> null
 105       /\ istree m l /\ istree m r
 106       /\ root l = m[p].left /\ root r = m[p].right
 107     end
 108
 109   let rec lemma extensionality (m m': memory) (t: tree loc) : unit
 110     requires { istree m t }
 111     requires { forall p. Mem.mem p (inorder t) ->
 112       m[p].left = m'[p].left /\ m[p].right = m'[p].right }
 113     ensures  { istree m' t }
 114     variant { t }
 115   = let rc = extensionality m m' in
 116     match t with Empty -> () | Node l _ r -> rc l; rc r end
 117
 118   (* degenerated zipper for a left descent (= list of pairs) *)
 119   type zipper 'a =
 120     | Top
 121     | Left (zipper 'a) 'a (tree 'a)
 122
 123   let rec function zip (t: tree 'a) (z: zipper 'a) : tree 'a
 124   = match z with
 125     | Top -> t
 126     | Left z x r -> zip (Node t x r) z
 127     end
 128
 129   function inorderz (z: zipper 'a) : list 'a =
 130     match z with
 131     | Top -> Nil
 132     | Left z x r -> Cons x (inorder r) ++ inorderz z
 133     end
 134
 135   lemma inorder_zip:
 136      forall z [@induction]: zipper 'a, t: tree 'a.
 137        inorder (zip t z) = inorder t ++ inorderz z
 138
 139   let ghost tree_left (t: tree loc) : tree loc
 140     requires { t <> Empty }
 141     ensures  { match t with Empty -> false | Node l _ _ -> result = l end }
 142   = match t with Empty -> absurd | Node l _ _ -> l end
 143
 144   let ghost tree_right (t: tree loc) : tree loc
 145     requires { t <> Empty }
 146     ensures  { match t with Empty -> false | Node _ _ r -> result = r end }
 147   = match t with Empty -> absurd | Node _ _ r -> r end
 148
 149   lemma distinct_break_append :
 150     forall l1 [@induction] l2:list 'a.
 151     distinct (l1 ++ l2) ->
 152     distinct l1 /\ distinct l2 /\ forall x. Mem.mem x l1 -> not Mem.mem x l2
 153
 154   let rec ghost in_zip_tree (m: memory) (t: tree loc) (z: zipper loc) : unit
 155     requires { istree m (zip t z) }
 156     ensures  { istree m t }
 157     variant  { z }
 158   = match z with Top -> () | Left z p r -> in_zip_tree m (Node t p r) z end
 159
 160   let rec ghost subst_zip_tree (m m': memory)
 161                                (t1 t2: tree loc) (z: zipper loc) : unit
 162     requires { istree m (zip t1 z) /\ istree m' t2 }
 163     requires { root t1 = root t2 }
 164     requires { distinct (inorder (zip t1 z)) }
 165     requires { forall x. m[x] <> m'[x] -> Mem.mem x (inorder t1) }
 166     ensures  { istree m' (zip t2 z) /\ root (zip t1 z) = root (zip t2 z) }
 167     variant  { z }
 168   = match z with
 169     | Top -> ()
 170     | Left z p r ->
 171       let t3 = Node t1 p r in
 172       in_zip_tree m t3 z;
 173       assert { forall q. Mem.mem q (inorder r) \/ q = p ->
 174         m[q] = m'[q] by Mem.mem q (Cons p (inorder r)) /\ distinct (inorder t3)
 175       };
 176       extensionality m m' r;
 177       subst_zip_tree m m' t3 (Node t2 p r) z
 178     end
 179
 180   let lemma main_lemma (m: memory) (pp p: loc)
 181                        (ppr pr: tree loc) (z: zipper loc) : unit
 182     requires { let it = zip (Node (Node Empty p pr) pp ppr) z in
 183       istree m it /\ distinct (inorder it) }
 184     ensures { let m' = m[pp <- { m[pp] with left = m[p].right }] in
 185       let t1 = Node (Node Empty p pr) pp ppr in
 186       let t2 = Node pr pp ppr in
 187       istree m' (zip t2 z) /\ root (zip t1 z) = root (zip t2 z)
 188     }
 189   = let m' = m[pp <- { m[pp] with left = m[p].right }] in
 190     let t1 = Node (Node Empty p pr) pp ppr in
 191     in_zip_tree m t1 z;
 192     assert { let l = inorder pr ++ Cons pp (inorder ppr) in
 193       distinct l by distinct (inorder t1) so inorder t1 = Cons p l };
 194     extensionality m m' pr;
 195     extensionality m m' ppr;
 196     subst_zip_tree m m' t1 (Node pr pp ppr) z
 197
 198   (* specification is as follows: if t is a tree and its list of locs
 199      is x::l then, at the end of execution, its list is l and m = x.data *)
 200   let search_tree_delete_min
 201     (t: loc) (ghost it: tree loc) (ghost ot: ref (tree loc))
 202     : (loc, int)
 203     requires { t <> null }
 204     requires { istree !mem it /\ t = root it }
 205     requires { distinct (inorder it) }
 206     ensures  { forall p. !mem[p].data = old !mem[p].data }
 207     ensures  { let (t', m) = result in istree !mem !ot /\ root !ot = t' /\
 208                match inorder it with
 209                | Nil -> false
 210                | Cons p l -> m = !mem[p].data /\ inorder !ot = l end }
 211     =
 212     label I in
 213     let p = ref (get_left t) in
 214     if eq_loc !p null then begin
 215       let m = get_data t in
 216       let tt = get_right t in
 217       ghost match it with Empty -> absurd
 218         | Node l _ r -> assert { l = Empty }; ot := r end;
 219       (tt, m)
 220     end else begin
 221       let pp = ref t in
 222       let tt = ref (get_left !p) in
 223       let ghost zipper = ref Top in
 224       let ghost ppr = ref (tree_right it) in
 225       let ghost subtree = ref (tree_left it) in
 226       while not (eq_loc !tt null) do
 227         invariant { !pp <> null /\ !mem[!pp].left = !p }
 228         invariant { !p <> null /\ !mem[!p].left = !tt }
 229         invariant { let pt = Node !subtree !pp !ppr in
 230                     istree !mem pt /\ zip pt !zipper = it }
 231         invariant { forall p. !mem[p].data = (!mem[p].data at I) }
 232         variant { !subtree }
 233         assert { istree !mem !subtree /\ root !subtree = !p };
 234         ghost zipper := Left !zipper !pp !ppr;
 235         ghost ppr := tree_right !subtree;
 236         ghost subtree := tree_left !subtree;
 237         pp := !p;
 238         p := !tt;
 239         tt := get_left !p
 240       done;
 241       assert { istree !mem !subtree /\ root !subtree = !p };
 242       assert { !pp <> !p };
 243       let m = get_data !p in
 244       tt := get_right !p;
 245       set_left !pp !tt;
 246       let ghost pl = tree_left !subtree in assert { pl = Empty };
 247       let ghost z = Left !zipper !pp !ppr in
 248       ghost ot := zip (tree_right !subtree) z;
 249       (t, m)
 250     end
 251
 252 end