Wiki Agenda Contact Version française

VerifyThis @ FM 2012, problem 3

Iterative deletion in a binary search tree


Authors: Jean-Christophe Filliâtre / Andrei Paskevich

Topics: Trees / Ghost code

Tools: Why3

References: VerifyThis @ FM2012

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


download ZIP archive
(* {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 *)

(*
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

Why3 Proof Results for Project "verifythis_fm2012_treedel"

Theory "verifythis_fm2012_treedel.Memory": fully verified in 0.02 s

ObligationsAlt-Ergo (0.99.1)CVC3 (2.4.1)CVC4 (1.4)Eprover (1.8-001)Vampire (0.6)Z3 (3.2)Z3 (4.3.2)
VC for get_left0.010.000.000.000.000.000.00
VC for get_right0.000.000.000.000.000.000.00
VC for get_data0.010.000.000.000.000.000.00

Theory "verifythis_fm2012_treedel.Treedel": fully verified in 32.58 s

ObligationsAlt-Ergo (0.99.1)CVC3 (2.4.1)CVC4 (1.4)Coq (8.4pl6)Eprover (1.8-001)Vampire (0.6)Z3 (3.2)Z3 (4.3.2)
inorder_zip------------------------
induction_ty_lex
  1.------------------------
split_goal_wp
  1.0.010.020.03---0.000.010.020.04
2.0.061.040.12---------------
VC for tree_left0.020.020.03---0.020.030.020.01
VC for tree_right0.010.020.02---0.010.030.020.01
main_lemma---------12.25------------
VC for search_tree_delete_min------------------------
split_goal_wp
  1. precondition0.010.020.02---0.010.000.020.04
2. precondition0.020.020.02---0.010.000.000.00
3. precondition0.010.010.02---0.010.000.000.00
4. unreachable point0.020.040.03---0.050.060.020.06
5. assertion0.020.060.03---0.020.900.040.06
6. postcondition0.270.040.04------0.930.020.05
7. precondition0.010.030.03---0.010.010.000.00
8. precondition0.01---0.03---0.040.050.020.06
9. precondition0.020.030.02---0.010.000.010.02
10. loop invariant init0.020.030.03---0.010.000.010.02
11. loop invariant init0.020.010.02---0.010.010.010.02
12. loop invariant init0.080.140.04---0.022.930.100.12
13. assertion0.030.060.04---------0.020.05
14. precondition0.020.090.04---0.080.060.050.04
15. precondition0.020.020.03---0.010.000.070.03
16. precondition0.010.020.02---0.010.000.020.03
17. loop invariant preservation0.020.020.03---0.010.010.020.03
18. loop invariant preservation0.020.020.03---0.010.010.020.03
19. loop invariant preservation0.100.050.06---0.232.97------
20. loop variant decrease0.020.030.04---0.020.020.020.01
21. assertion0.030.060.04---------0.020.04
22. assertion0.020.020.02---0.010.000.020.05
23. precondition0.010.010.03---0.010.000.010.04
24. precondition0.020.020.02---0.010.000.000.00
25. precondition0.050.050.04---0.060.050.040.05
26. assertion0.200.040.05---0.020.990.090.11
27. precondition0.020.040.02---0.010.000.000.02
28. postcondition------------------------
split_goal_wp
  1. VC for search_tree_delete_min0.10---0.05---------------
2. VC for search_tree_delete_min------0.09---0.032.680.110.02
3. VC for search_tree_delete_min------0.08------0.940.080.08
4. VC for search_tree_delete_min------0.10---0.11---------