## VerifyThis @ FM 2012, problem 3

Iterative deletion in a binary search tree

Topics: Trees / Ghost code / Pointer Programs

Tools: Why3

References: VerifyThis @ FM2012

see also the index (by topic, by tool, by reference, by year)

# The VerifyThis competition at FM2012: Problem 3

Author: Jean-Christophe FilliĆ¢tre

```(*
Iterative deletion in a binary search tree - 90 minutes

-----------------

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
```

# Why3 Proof Results for Project "verifythis_fm2012_treedel"

## Theory "verifythis_fm2012_treedel.Memory": fully verified

 Obligations Alt-Ergo 2.0.0 VC null 0.00 VC get_left 0.00 VC get_right 0.00 VC get_data 0.00

## Theory "verifythis_fm2012_treedel.Treedel": fully verified

 Obligations Alt-Ergo 2.0.0 CVC4 1.5 Eprover 1.8-001 VC extensionality --- --- --- split_goal_right VC extensionality.0 0.01 --- --- VC extensionality.1 0.01 --- --- VC extensionality.2 0.02 --- --- VC extensionality.3 0.01 --- --- VC extensionality.4 0.01 --- --- VC extensionality.5 0.01 --- --- VC extensionality.6 0.02 --- --- VC zip --- 0.01 --- inorder_zip --- --- --- induction_ty_lex inorder_zip.0 0.01 --- --- VC tree_left 0.01 --- --- VC tree_right 0.00 --- --- distinct_break_append --- --- --- induction_ty_lex distinct_break_append.0 0.19 --- --- VC in_zip_tree --- --- --- split_goal_right VC in_zip_tree.0 0.01 --- --- VC in_zip_tree.1 0.01 --- --- VC in_zip_tree.2 0.01 --- --- VC subst_zip_tree --- --- --- split_goal_right VC subst_zip_tree.0 0.00 --- --- VC subst_zip_tree.1 --- --- --- split_goal_right VC subst_zip_tree.1.0 0.02 --- --- VC subst_zip_tree.1.1 0.01 --- --- VC subst_zip_tree.1.2 0.01 --- --- VC subst_zip_tree.2 0.01 --- --- VC subst_zip_tree.3 0.01 --- --- VC subst_zip_tree.4 0.01 --- --- VC subst_zip_tree.5 0.01 --- --- VC subst_zip_tree.6 0.01 --- --- VC subst_zip_tree.7 0.01 --- --- VC subst_zip_tree.8 0.01 --- --- VC subst_zip_tree.9 0.00 --- --- VC main_lemma --- --- --- split_goal_right VC main_lemma.0 0.01 --- --- VC main_lemma.1 --- --- --- split_goal_right VC main_lemma.1.0 0.02 --- --- VC main_lemma.1.1 0.04 --- --- VC main_lemma.1.2 0.04 --- --- VC main_lemma.2 0.01 --- --- VC main_lemma.3 0.17 --- --- VC main_lemma.4 0.01 --- --- VC main_lemma.5 0.22 --- --- VC main_lemma.6 0.03 --- --- VC main_lemma.7 0.01 --- --- VC main_lemma.8 0.01 --- --- VC main_lemma.9 0.04 --- --- VC main_lemma.10 0.01 --- --- VC search_tree_delete_min --- --- --- split_goal_right VC search_tree_delete_min.0 0.01 --- --- VC search_tree_delete_min.1 0.01 --- --- VC search_tree_delete_min.2 0.00 --- --- VC search_tree_delete_min.3 0.00 --- --- VC search_tree_delete_min.4 --- --- 0.03 VC search_tree_delete_min.5 0.01 --- --- VC search_tree_delete_min.6 0.04 --- --- VC search_tree_delete_min.7 0.01 --- --- VC search_tree_delete_min.8 0.01 --- --- VC search_tree_delete_min.9 0.01 --- --- VC search_tree_delete_min.10 0.01 --- --- VC search_tree_delete_min.11 0.01 --- --- VC search_tree_delete_min.12 0.07 --- --- VC search_tree_delete_min.13 0.00 --- --- VC search_tree_delete_min.14 0.02 --- --- VC search_tree_delete_min.15 0.03 --- --- VC search_tree_delete_min.16 0.02 --- --- VC search_tree_delete_min.17 0.01 --- --- VC search_tree_delete_min.18 0.03 --- --- VC search_tree_delete_min.19 0.01 --- --- VC search_tree_delete_min.20 0.01 --- --- VC search_tree_delete_min.21 0.13 --- --- VC search_tree_delete_min.22 0.00 --- --- VC search_tree_delete_min.23 0.02 --- --- VC search_tree_delete_min.24 0.01 --- --- VC search_tree_delete_min.25 0.01 --- --- VC search_tree_delete_min.26 0.01 --- --- VC search_tree_delete_min.27 0.01 --- --- VC search_tree_delete_min.28 0.02 --- --- VC search_tree_delete_min.29 --- --- 0.90 VC search_tree_delete_min.30 0.01 --- --- VC search_tree_delete_min.31 0.01 --- --- VC search_tree_delete_min.32 --- --- --- split_goal_right VC search_tree_delete_min.32.0 0.27 --- --- VC search_tree_delete_min.32.1 0.01 --- --- VC search_tree_delete_min.32.2 0.07 --- --- VC search_tree_delete_min.32.3 --- 0.55 --- VC search_tree_delete_min.32.4 --- 0.83 ---