verifythis_fm2012_treedel.mlw 5.16 KB
 Jean-Christophe Filliatre committed Nov 19, 2012 1 2 3 4 5 6 7 `````` (* {1 The VerifyThis competition at FM2012: Problem 3} See {h this web page} Author: Jean-Christophe Filliâtre *) `````` Jean-Christophe Filliatre committed Jan 30, 2013 8 ``````(* `````` MARCHE Claude committed Feb 12, 2013 9 ``````Iterative deletion in a binary search tree - 90 minutes `````` Jean-Christophe Filliatre committed Jan 30, 2013 10 11 12 13 14 `````` VERIFICATION TASK ----------------- `````` Andrei Paskevich committed Feb 15, 2013 15 ``````Given: a pointer t to the root of a non-empty binary search tree (not `````` Jean-Christophe Filliatre committed Jan 30, 2013 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. *) `````` Andrei Paskevich committed Feb 15, 2013 41 ``````(* Why3 has no pointer data structures, so we model the heap *) `````` Jean-Christophe Filliatre committed Nov 19, 2012 42 43 44 45 46 ``````module Memory use export map.Map use export ref.Ref `````` MARCHE Claude committed Feb 15, 2013 47 48 49 50 `````` type loc constant null: loc type node = { left: loc; right: loc; data: int; } type memory = map loc node `````` Jean-Christophe Filliatre committed Nov 19, 2012 51 52 53 54 `````` (* the global variable mem contains the current state of the memory *) val mem: ref memory `````` MARCHE Claude committed Feb 15, 2013 55 56 `````` (* accessor functions to ensure safety i.e. no null loc dereference *) let get_left (p: loc) : loc = `````` Jean-Christophe Filliatre committed Nov 19, 2012 57 `````` requires { p <> null } `````` Jean-Christophe Filliatre committed Nov 21, 2012 58 59 `````` ensures { result = !mem[p].left } !mem[p].left `````` MARCHE Claude committed Feb 15, 2013 60 `````` let get_right (p: loc) : loc = `````` Jean-Christophe Filliatre committed Nov 19, 2012 61 `````` requires { p <> null } `````` Jean-Christophe Filliatre committed Nov 21, 2012 62 63 `````` ensures { result = !mem[p].right } !mem[p].right `````` MARCHE Claude committed Feb 15, 2013 64 `````` let get_data (p: loc) : int = `````` Jean-Christophe Filliatre committed Nov 19, 2012 65 `````` requires { p <> null } `````` Jean-Christophe Filliatre committed Nov 21, 2012 66 67 `````` ensures { result = !mem[p].data } !mem[p].data `````` Jean-Christophe Filliatre committed Nov 19, 2012 68 69 70 71 72 73 74 75 `````` end module Treedel use import Memory use import bintree.Tree use import bintree.Inorder `````` Guillaume Melquiond committed Aug 21, 2014 76 77 `````` use import list.List use import list.Append `````` Jean-Christophe Filliatre committed Nov 19, 2012 78 79 80 `````` use import list.Distinct (* there is a binary tree t rooted at p in memory m *) `````` MARCHE Claude committed Feb 15, 2013 81 `````` inductive istree (m: memory) (p: loc) (t: tree loc) = `````` Jean-Christophe Filliatre committed Nov 21, 2012 82 `````` | leaf: forall m: memory. `````` MARCHE Claude committed Feb 15, 2013 83 84 `````` istree m null Empty | node: forall m: memory, p: loc, l r: tree loc. `````` Jean-Christophe Filliatre committed Nov 19, 2012 85 `````` p <> null -> `````` MARCHE Claude committed Feb 15, 2013 86 87 88 `````` istree m m[p].left l -> istree m m[p].right r -> istree m p (Node l p r) `````` Jean-Christophe Filliatre committed Nov 19, 2012 89 `````` `````` Jean-Christophe Filliatre committed Nov 23, 2012 90 `````` (* degenerated zipper for a left descent (= list of pairs) *) `````` Jean-Christophe Filliatre committed Nov 21, 2012 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 `````` Jean-Christophe Filliatre committed Nov 19, 2012 99 `````` `````` Jean-Christophe Filliatre committed Nov 21, 2012 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)) `````` Jean-Christophe Filliatre committed Nov 19, 2012 103 `````` `````` Andrei Paskevich committed Nov 20, 2013 104 `````` let ghost tree_left (t: tree loc) : tree loc `````` Jean-Christophe Filliatre committed Nov 19, 2012 105 106 `````` requires { t <> Empty } ensures { match t with Empty -> false | Node l _ _ -> result = l end } `````` MARCHE Claude committed Mar 10, 2013 107 `````` = `````` Jean-Christophe Filliatre committed Nov 19, 2012 108 109 `````` match t with Empty -> absurd | Node l _ _ -> l end `````` Andrei Paskevich committed Nov 20, 2013 110 `````` let ghost tree_right (t: tree loc) : tree loc `````` Jean-Christophe Filliatre committed Nov 19, 2012 111 112 `````` requires { t <> Empty } ensures { match t with Empty -> false | Node _ _ r -> result = r end } `````` MARCHE Claude committed Mar 10, 2013 113 `````` = `````` Jean-Christophe Filliatre committed Nov 19, 2012 114 115 `````` match t with Empty -> absurd | Node _ _ r -> r end `````` Jean-Christophe Filliatre committed Nov 21, 2012 116 `````` lemma main_lemma: `````` MARCHE Claude committed Feb 15, 2013 117 `````` forall m: memory, t pp p: loc, ppr pr: tree loc, z: zipper loc. `````` Jean-Christophe Filliatre committed Nov 23, 2012 118 `````` let it = zip (Node (Node Empty p pr) pp ppr) z in `````` MARCHE Claude committed Feb 15, 2013 119 `````` istree m t it -> distinct (inorder it) -> `````` Jean-Christophe Filliatre committed Nov 21, 2012 120 `````` let m' = m[pp <- { m[pp] with left = m[p].right }] in `````` MARCHE Claude committed Feb 15, 2013 121 `````` istree m' t (zip (Node pr pp ppr) z) `````` Jean-Christophe Filliatre committed Nov 21, 2012 122 `````` `````` MARCHE Claude committed Feb 15, 2013 123 `````` (* specification is as follows: if t is a tree and its list of locs `````` Jean-Christophe Filliatre committed Nov 19, 2012 124 125 `````` is x::l then, at the end of execution, its list is l and m = x.data *) let search_tree_delete_min `````` MARCHE Claude committed Feb 15, 2013 126 127 `````` (t: loc) (ghost it: tree loc) (ghost ot: ref (tree loc)) : (loc, int) `````` Jean-Christophe Filliatre committed Nov 19, 2012 128 `````` requires { t <> null } `````` MARCHE Claude committed Feb 15, 2013 129 `````` requires { istree !mem t it } `````` Jean-Christophe Filliatre committed Nov 21, 2012 130 `````` requires { distinct (inorder it) } `````` MARCHE Claude committed Feb 15, 2013 131 `````` ensures { let (t', m) = result in istree !mem t' !ot /\ `````` Jean-Christophe Filliatre committed Nov 21, 2012 132 `````` match inorder it with `````` Jean-Christophe Filliatre committed Nov 19, 2012 133 `````` | Nil -> false `````` Jean-Christophe Filliatre committed Nov 21, 2012 134 `````` | Cons p l -> m = !mem[p].data /\ inorder !ot = l end } `````` Jean-Christophe Filliatre committed Feb 12, 2013 135 `````` = `````` Jean-Christophe Filliatre committed Nov 19, 2012 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 `````` Jean-Christophe Filliatre committed Nov 21, 2012 140 141 `````` ghost match it with Empty -> absurd | Node l _ r -> assert { l = Empty }; ot := r end; `````` Jean-Christophe Filliatre committed Nov 19, 2012 142 143 144 145 `````` (tt, m) end else begin let pp = ref t in let tt = ref (get_left !p) in `````` Jean-Christophe Filliatre committed Nov 21, 2012 146 `````` let ghost zipper = ref Top in `````` Andrei Paskevich committed Nov 20, 2013 147 148 `````` let ghost ppr = ref (tree_right it) in let ghost subtree = ref (tree_left it) in `````` Jean-Christophe Filliatre committed Nov 19, 2012 149 `````` while !tt <> null do `````` MARCHE Claude committed Feb 12, 2013 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 `````` MARCHE Claude committed Feb 15, 2013 153 `````` istree !mem !pp pt /\ zip pt !zipper = it } `````` MARCHE Claude committed Jan 21, 2014 154 `````` variant { !subtree } `````` MARCHE Claude committed Feb 15, 2013 155 `````` assert { istree !mem !p !subtree }; `````` Jean-Christophe Filliatre committed Nov 21, 2012 156 `````` ghost zipper := Left !zipper !pp !ppr; `````` Andrei Paskevich committed Nov 20, 2013 157 158 `````` ghost ppr := tree_right !subtree; ghost subtree := tree_left !subtree; `````` Jean-Christophe Filliatre committed Nov 19, 2012 159 160 161 162 `````` pp := !p; p := !tt; tt := get_left !p done; `````` MARCHE Claude committed Feb 15, 2013 163 `````` assert { istree !mem !p !subtree }; `````` Jean-Christophe Filliatre committed Nov 21, 2012 164 `````` assert { !pp <> !p }; `````` Jean-Christophe Filliatre committed Nov 19, 2012 165 166 `````` let m = get_data !p in tt := get_right !p; `````` Jean-Christophe Filliatre committed Nov 21, 2012 167 `````` mem := set !mem !pp { !mem[!pp] with left = !tt }; `````` Andrei Paskevich committed Nov 20, 2013 168 169 `````` let ghost pl = tree_left !subtree in assert { pl = Empty }; ghost ot := zip (tree_right !subtree) (Left !zipper !pp !ppr); `````` Jean-Christophe Filliatre committed Nov 19, 2012 170 171 172 173 `````` (t, m) end end``````