verifythis_fm2012_treedel.mlw 5.16 KB
Newer Older
1 2 3 4 5 6 7

(* {1 The VerifyThis competition at FM2012: Problem 3}

   See {h <a href="http://fm2012.verifythis.org/challenges">this web page</a>}

   Author: Jean-Christophe Filliâtre *)

8
(*
9
Iterative deletion in a binary search tree - 90 minutes
10 11 12 13 14


VERIFICATION TASK
-----------------

15
Given: a pointer t to the root of a non-empty binary search tree (not
16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40
necessarily balanced). Verify that the following procedure removes the
node with the minimal key from the tree. After removal, the data
structure should again be a binary search tree.


(Tree, int) search_tree_delete_min (Tree t) {
   Tree tt, pp, p;
   int m;
   p = t->left;
   if (p == NULL) {
       m = t->data; tt = t->right; dispose (t); t = tt;
   } else {
       pp = t; tt = p->left;
       while (tt != NULL) {
           pp = p; p = tt; tt = p->left;
       }
       m = p->data; tt = p->right; dispose(p); pp->left= tt;
   }
   return (t,m);
}

Note: When implementing in a garbage-collected language, the call to
dispose() is superfluous.
*)

41
(* Why3 has no pointer data structures, so we model the heap *)
42 43 44 45 46
module Memory

  use export map.Map
  use export ref.Ref

47 48 49 50
  type loc
  constant null: loc
  type node = { left: loc; right: loc; data: int; }
  type memory = map loc node
51 52 53 54

  (* the global variable mem contains the current state of the memory *)
  val mem: ref memory

55 56
  (* accessor functions to ensure safety i.e. no null loc dereference *)
  let get_left (p: loc) : loc =
57
    requires { p <> null }
58 59
    ensures  { result = !mem[p].left }
    !mem[p].left
60
  let get_right (p: loc) : loc =
61
    requires { p <> null }
62 63
    ensures  { result = !mem[p].right }
    !mem[p].right
64
  let get_data (p: loc) : int =
65
    requires { p <> null }
66 67
    ensures  { result = !mem[p].data }
    !mem[p].data
68 69 70 71 72 73 74 75

end

module Treedel

  use import Memory
  use import bintree.Tree
  use import bintree.Inorder
76 77
  use import list.List
  use import list.Append
78 79 80
  use import list.Distinct

  (* there is a binary tree t rooted at p in memory m *)
81
  inductive istree (m: memory) (p: loc) (t: tree loc) =
82
    | leaf: forall m: memory.
83 84
        istree m null Empty
    | node: forall m: memory, p: loc, l r: tree loc.
85
        p <> null ->
86 87 88
        istree m m[p].left l ->
        istree m m[p].right r ->
        istree m p (Node l p r)
89

90
  (* degenerated zipper for a left descent (= list of pairs) *)
91 92 93 94 95 96 97 98
  type zipper 'a =
    | Top
    | Left (zipper 'a) 'a (tree 'a)

  function zip (t: tree 'a) (z: zipper 'a) : tree 'a = match z with
    | Top -> t
    | Left z x r -> zip (Node t x r) z
  end
99

100 101 102
  lemma inorder_zip:
     forall z "induction": zipper 'a, x: 'a, l r: tree 'a.
     inorder (zip (Node l x r) z) = inorder l ++ Cons x (inorder (zip r z))
103

104
  let ghost tree_left (t: tree loc) : tree loc
105 106
     requires { t <> Empty }
     ensures  { match t with Empty -> false | Node l _ _ -> result = l end }
MARCHE Claude's avatar
MARCHE Claude committed
107
  =
108 109
     match t with Empty -> absurd | Node l _ _ -> l end

110
  let ghost tree_right (t: tree loc) : tree loc
111 112
     requires { t <> Empty }
     ensures  { match t with Empty -> false | Node _ _ r -> result = r end }
MARCHE Claude's avatar
MARCHE Claude committed
113
  =
114 115
     match t with Empty -> absurd | Node _ _ r -> r end

116
  lemma main_lemma:
117
    forall m: memory, t pp p: loc, ppr pr: tree loc, z: zipper loc.
118
    let it = zip (Node (Node Empty p pr) pp ppr) z in
119
    istree m t it -> distinct (inorder it) ->
120
    let m' = m[pp <- { m[pp] with left = m[p].right }] in
121
    istree m' t (zip (Node pr pp ppr) z)
122

123
  (* specification is as follows: if t is a tree and its list of locs
124 125
     is x::l then, at the end of execution, its list is l and m = x.data *)
  let search_tree_delete_min
126 127
    (t: loc) (ghost it: tree loc) (ghost ot: ref (tree loc))
    : (loc, int)
128
    requires { t <> null }
129
    requires { istree !mem t it }
130
    requires { distinct (inorder it) }
131
    ensures  { let (t', m) = result in istree !mem t' !ot /\
132
               match inorder it with
133
               | Nil -> false
134
               | Cons p l -> m = !mem[p].data /\ inorder !ot = l end }
135
    =
136 137 138 139
    let p = ref (get_left t) in
    if !p = null then begin
      let m = get_data t in
      let tt = get_right t in
140 141
      ghost match it with Empty -> absurd
        | Node l _ r -> assert { l = Empty }; ot := r end;
142 143 144 145
      (tt, m)
    end else begin
      let pp = ref t in
      let tt = ref (get_left !p) in
146
      let ghost zipper = ref Top in
147 148
      let ghost ppr = ref (tree_right it) in
      let ghost subtree = ref (tree_left it) in
149
      while !tt <> null do
150 151 152
        invariant { !pp <> null /\ !mem[!pp].left = !p }
        invariant { !p <> null /\ !mem[!p].left = !tt }
        invariant { let pt = Node !subtree !pp !ppr in
153
                    istree !mem !pp pt /\ zip pt !zipper = it }
154
        variant { !subtree }
155
        assert { istree !mem !p !subtree };
156
        ghost zipper := Left !zipper !pp !ppr;
157 158
        ghost ppr := tree_right !subtree;
        ghost subtree := tree_left !subtree;
159 160 161 162
        pp := !p;
        p := !tt;
        tt := get_left !p
      done;
163
      assert { istree !mem !p !subtree };
164
      assert { !pp <> !p };
165 166
      let m = get_data !p in
      tt := get_right !p;
167
      mem := set !mem !pp { !mem[!pp] with left = !tt };
168 169
      let ghost pl = tree_left !subtree in assert { pl = Empty };
      ghost ot := zip (tree_right !subtree) (Left !zipper !pp !ppr);
170 171 172 173
      (t, m)
    end

end