(** {1 The VerifyThis competition at FM2012: Problem 3} See {h this web page} Author: Jean-Christophe FilliĆ¢tre *) (* Iterative deletion in a binary search tree - 90 minutes VERIFICATION TASK ----------------- Given: a pointer t to the root of a non-empty binary search tree (not 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. *) (* Why3 has no pointer data structures, so we model the heap *) module Memory use export map.Map use export ref.Ref type loc val constant null: loc val predicate eq_loc (x y:loc) ensures { result <-> x = y } type node = { left: loc; right: loc; data: int; } type memory = map loc node (* the global variable mem contains the current state of the memory *) val mem: ref memory (* accessor functions to ensure safety i.e. no null loc dereference *) let get_left (p: loc) : loc = requires { p <> null } ensures { result = !mem[p].left } !mem[p].left let get_right (p: loc) : loc = requires { p <> null } ensures { result = !mem[p].right } !mem[p].right let get_data (p: loc) : int = requires { p <> null } ensures { result = !mem[p].data } !mem[p].data val set_left (p: loc) (v:loc) : unit requires { p <> null } writes { mem } ensures { !mem[p] = { (old !mem)[p] with left = v } } ensures { forall q. q <> p -> !mem[q] = (old !mem)[q] } (* FIXME: This expression makes a ghost modification in the non-ghost variable mem = mem := set !mem p { !mem[p] with left = v } *) end module Treedel use Memory use bintree.Tree use bintree.Inorder use list.List use list.Mem use list.Append use list.Distinct function root (t: tree loc) : loc = match t with | Empty -> null | Node _ p _ -> p end (* there is a binary tree t in memory m *) predicate istree (m: memory) (t: tree loc) = match t with | Empty -> true | Node l p r -> p <> null /\ istree m l /\ istree m r /\ root l = m[p].left /\ root r = m[p].right end let rec lemma extensionality (m m': memory) (t: tree loc) : unit requires { istree m t } requires { forall p. Mem.mem p (inorder t) -> m[p].left = m'[p].left /\ m[p].right = m'[p].right } ensures { istree m' t } variant { t } = let rc = extensionality m m' in match t with Empty -> () | Node l _ r -> rc l; rc r end (* degenerated zipper for a left descent (= list of pairs) *) type zipper 'a = | Top | Left (zipper 'a) 'a (tree 'a) let rec 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 function inorderz (z: zipper 'a) : list 'a = match z with | Top -> Nil | Left z x r -> Cons x (inorder r) ++ inorderz z end lemma inorder_zip: forall z [@induction]: zipper 'a, t: tree 'a. inorder (zip t z) = inorder t ++ inorderz z let ghost tree_left (t: tree loc) : tree loc requires { t <> Empty } ensures { match t with Empty -> false | Node l _ _ -> result = l end } = match t with Empty -> absurd | Node l _ _ -> l end let ghost tree_right (t: tree loc) : tree loc requires { t <> Empty } ensures { match t with Empty -> false | Node _ _ r -> result = r end } = match t with Empty -> absurd | Node _ _ r -> r end lemma distinct_break_append : forall l1 [@induction] l2:list 'a. distinct (l1 ++ l2) -> distinct l1 /\ distinct l2 /\ forall x. Mem.mem x l1 -> not Mem.mem x l2 let rec ghost in_zip_tree (m: memory) (t: tree loc) (z: zipper loc) : unit requires { istree m (zip t z) } ensures { istree m t } variant { z } = match z with Top -> () | Left z p r -> in_zip_tree m (Node t p r) z end let rec ghost subst_zip_tree (m m': memory) (t1 t2: tree loc) (z: zipper loc) : unit requires { istree m (zip t1 z) /\ istree m' t2 } requires { root t1 = root t2 } requires { distinct (inorder (zip t1 z)) } requires { forall x. m[x] <> m'[x] -> Mem.mem x (inorder t1) } ensures { istree m' (zip t2 z) /\ root (zip t1 z) = root (zip t2 z) } variant { z } = match z with | Top -> () | Left z p r -> let t3 = Node t1 p r in in_zip_tree m t3 z; assert { forall q. Mem.mem q (inorder r) \/ q = p -> m[q] = m'[q] by Mem.mem q (Cons p (inorder r)) /\ distinct (inorder t3) }; extensionality m m' r; subst_zip_tree m m' t3 (Node t2 p r) z end let lemma main_lemma (m: memory) (pp p: loc) (ppr pr: tree loc) (z: zipper loc) : unit requires { let it = zip (Node (Node Empty p pr) pp ppr) z in istree m it /\ distinct (inorder it) } ensures { let m' = m[pp <- { m[pp] with left = m[p].right }] in let t1 = Node (Node Empty p pr) pp ppr in let t2 = Node pr pp ppr in istree m' (zip t2 z) /\ root (zip t1 z) = root (zip t2 z) } = let m' = m[pp <- { m[pp] with left = m[p].right }] in let t1 = Node (Node Empty p pr) pp ppr in in_zip_tree m t1 z; assert { let l = inorder pr ++ Cons pp (inorder ppr) in distinct l by distinct (inorder t1) so inorder t1 = Cons p l }; extensionality m m' pr; extensionality m m' ppr; subst_zip_tree m m' t1 (Node pr pp ppr) z (* specification is as follows: if t is a tree and its list of locs is x::l then, at the end of execution, its list is l and m = x.data *) let search_tree_delete_min (t: loc) (ghost it: tree loc) (ghost ot: ref (tree loc)) : (loc, int) requires { t <> null } requires { istree !mem it /\ t = root it } requires { distinct (inorder it) } ensures { forall p. !mem[p].data = old !mem[p].data } ensures { let (t', m) = result in istree !mem !ot /\ root !ot = t' /\ match inorder it with | Nil -> false | Cons p l -> m = !mem[p].data /\ inorder !ot = l end } = label I in let p = ref (get_left t) in if eq_loc !p null then begin let m = get_data t in let tt = get_right t in ghost match it with Empty -> absurd | Node l _ r -> assert { l = Empty }; ot := r end; (tt, m) end else begin let pp = ref t in let tt = ref (get_left !p) in let ghost zipper = ref Top in let ghost ppr = ref (tree_right it) in let ghost subtree = ref (tree_left it) in while not (eq_loc !tt null) do invariant { !pp <> null /\ !mem[!pp].left = !p } invariant { !p <> null /\ !mem[!p].left = !tt } invariant { let pt = Node !subtree !pp !ppr in istree !mem pt /\ zip pt !zipper = it } invariant { forall p. !mem[p].data = (!mem[p].data at I) } variant { !subtree } assert { istree !mem !subtree /\ root !subtree = !p }; ghost zipper := Left !zipper !pp !ppr; ghost ppr := tree_right !subtree; ghost subtree := tree_left !subtree; pp := !p; p := !tt; tt := get_left !p done; assert { istree !mem !subtree /\ root !subtree = !p }; assert { !pp <> !p }; let m = get_data !p in tt := get_right !p; set_left !pp !tt; let ghost pl = tree_left !subtree in assert { pl = Empty }; let ghost z = Left !zipper !pp !ppr in ghost ot := zip (tree_right !subtree) z; (t, m) end end