(* {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 constant null: loc 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 end module Treedel use import Memory use import bintree.Tree use import bintree.Inorder use import list.List use import list.Append use import list.Distinct (* there is a binary tree t rooted at p in memory m *) inductive istree (m: memory) (p: loc) (t: tree loc) = | leaf: forall m: memory. istree m null Empty | node: forall m: memory, p: loc, l r: tree loc. p <> null -> istree m m[p].left l -> istree m m[p].right r -> istree m p (Node l p r) (* degenerated zipper for a left descent (= list of pairs) *) 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 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)) 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 main_lemma: forall m: memory, t pp p: loc, ppr pr: tree loc, z: zipper loc. let it = zip (Node (Node Empty p pr) pp ppr) z in istree m t it -> distinct (inorder it) -> let m' = m[pp <- { m[pp] with left = m[p].right }] in istree m' t (zip (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 t it } requires { distinct (inorder it) } ensures { let (t', m) = result in istree !mem t' !ot /\ match inorder it with | Nil -> false | Cons p l -> m = !mem[p].data /\ inorder !ot = l end } = let p = ref (get_left t) in if !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 !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 !pp pt /\ zip pt !zipper = it } variant { !subtree } assert { istree !mem !p !subtree }; 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 !p !subtree }; assert { !pp <> !p }; let m = get_data !p in tt := get_right !p; mem := set !mem !pp { !mem[!pp] with left = !tt }; let ghost pl = tree_left !subtree in assert { pl = Empty }; ghost ot := zip (tree_right !subtree) (Left !zipper !pp !ppr); (t, m) end end