verifythis_fm2012_treedel.mlw 4.24 KB
Newer Older
1
2
3
4
5
6
7

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

8
(* Why3 has no pointer data structures, so we model the heap *)
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
module Memory

  use export map.Map
  use export ref.Ref

  type pointer
  constant null: pointer
  type node = { left: pointer; right: pointer; data: int; }
  type memory = map pointer 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 pointer dereference *)
  let get_left (p: pointer) =
    requires { p <> null }
25
26
    ensures  { result = !mem[p].left }
    !mem[p].left
27
28
  let get_right (p: pointer) =
    requires { p <> null }
29
30
    ensures  { result = !mem[p].right }
    !mem[p].right
31
32
  let get_data (p: pointer) =
    requires { p <> null }
33
34
    ensures  { result = !mem[p].data }
    !mem[p].data
35
36
37
38
39
40
41
42
43
44
45
46

end

module Treedel

  use import Memory
  use import bintree.Tree
  use import bintree.Inorder
  use import list.Distinct

  (* there is a binary tree t rooted at p in memory m *)
  inductive tree (m: memory) (p: pointer) (t: tree pointer) =
47
48
    | leaf: forall m: memory.
        tree m null Empty
49
50
    | node: forall m: memory, p: pointer, l r: tree pointer.
        p <> null ->
51
52
        tree m m[p].left l ->
        tree m m[p].right r ->
53
54
        tree m p (Node l p r)

55
  (* degenerated zipper for a left descent (= list of pairs) *)
56
57
58
59
60
61
62
63
  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
64

65
66
67
  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))
68

69
  let ghost left (t: tree pointer) =
70
71
72
73
     requires { t <> Empty }
     ensures  { match t with Empty -> false | Node l _ _ -> result = l end }
     match t with Empty -> absurd | Node l _ _ -> l end

74
  let ghost right (t: tree pointer) =
75
76
77
78
     requires { t <> Empty }
     ensures  { match t with Empty -> false | Node _ _ r -> result = r end }
     match t with Empty -> absurd | Node _ _ r -> r end

79
  lemma main_lemma:
80
    forall m: memory, t pp p: pointer, ppr pr: tree pointer, z: zipper pointer.
81
    let it = zip (Node (Node Empty p pr) pp ppr) z in
82
83
    tree m t it -> distinct (inorder it) ->
    let m' = m[pp <- { m[pp] with left = m[p].right }] in
84
    tree m' t (zip (Node pr pp ppr) z)
85

86
87
88
  (* specification is as follows: if t is a tree and its list of pointers
     is x::l then, at the end of execution, its list is l and m = x.data *)
  let search_tree_delete_min
89
    (t: pointer) (ghost it: tree pointer) (ghost ot: ref (tree pointer)) =
90
    requires { t <> null }
91
92
93
94
    requires { tree !mem t it }
    requires { distinct (inorder it) }
    ensures  { let (t, m) = result in tree !mem t !ot /\
               match inorder it with
95
               | Nil -> false
96
               | Cons p l -> m = !mem[p].data /\ inorder !ot = l end }
97
98
99
100
    let p = ref (get_left t) in
    if !p = null then begin
      let m = get_data t in
      let tt = get_right t in
101
102
      ghost match it with Empty -> absurd
        | Node l _ r -> assert { l = Empty }; ot := r end;
103
104
105
106
      (tt, m)
    end else begin
      let pp = ref t in
      let tt = ref (get_left !p) in
107
108
      let ghost zipper = ref Top in
      let ghost ppr = ref (right it) in
109
      let ghost subtree = ref (left it) in
110
      while !tt <> null do
111
112
        invariant { !pp <> null /\ !mem[!pp].left = !p /\
                    !p <> null /\ !mem[!p].left = !tt /\
113
114
115
116
                    let pt = Node !subtree !pp !ppr in
                    tree !mem !pp pt /\ zip pt !zipper = it }
        assert { tree !mem !p !subtree };
        ghost zipper := Left !zipper !pp !ppr;
117
118
        ghost ppr := right !subtree;
        ghost subtree := left !subtree;
119
120
121
122
        pp := !p;
        p := !tt;
        tt := get_left !p
      done;
123
124
      assert { tree !mem !p !subtree };
      assert { !pp <> !p };
125
126
      let m = get_data !p in
      tt := get_right !p;
127
      mem := set !mem !pp { !mem[!pp] with left = !tt };
128
129
      let ghost pl = left !subtree in assert { pl = Empty };
      ghost ot := zip (right !subtree) (Left !zipper !pp !ppr);
130
131
132
133
      (t, m)
    end

end