vstte12_tree_reconstruction.mlw 9.49 KB
Newer Older
1

2
(* The 2nd Verified Software Competition (VSTTE 2012)
3 4 5 6 7 8 9 10 11
   https://sites.google.com/site/vstte2012/compet

   Problem 4: Tree Reconstruction
   Build a binary tree from a list of leaf depths, if any

   This is a purely applicative implementation, using immutable
   lists from Why3's standard library.
*)

12
module Tree
13

14 15 16
  use export int.Int
  use export list.List
  use export list.Append
17 18 19 20

  type tree = Leaf | Node tree tree

  (* the list of leaf depths for tree t, if root is at depth d *)
21 22
  let rec function depths (d: int) (t: tree) : list int =
    match t with
23 24
    | Leaf -> Cons d Nil
    | Node l r -> depths (d+1) l ++ depths (d+1) r
25
    end
26

27 28
  (* lemmas on depths *)

29 30 31 32
  lemma depths_head:
    forall t: tree, d: int.
    match depths d t with Cons x _ -> x >= d | Nil -> false end

33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48
  let rec lemma depths_unique (t1 t2: tree) (d: int) (s1 s2: list int)
    requires { depths d t1 ++ s1 = depths d t2 ++ s2 }
    variant { t1 }
    ensures { t1 = t2 && s1 = s2 }
  = let d' = d+1 in
    match t1,t2 with
    | Leaf,Leaf -> ()
    | Node t11 t12, Node t21 t22 ->
      depths_unique t11 t21 d' (depths d' t12 ++ s1) (depths d' t22 ++ s2);
      depths_unique t12 t22 d' s1 s2
    | Leaf, (Node t _) | (Node t _), Leaf ->
      match depths d' t with
      | Nil -> absurd
      | Cons x _ -> assert { x >= d' }
      end
    end
49

50 51 52 53 54 55 56 57
  lemma depths_prefix:
    forall t: tree, d1 d2: int, s1 s2: list int.
    depths d1 t ++ s1 = depths d2 t ++ s2 -> d1 = d2

  lemma depths_prefix_simple:
    forall t: tree, d1 d2: int.
    depths d1 t = depths d2 t -> d1 = d2

58 59 60 61 62 63 64 65 66 67
  let rec lemma depths_subtree (t1 t2: tree) (d1 d2:int) (s1:list int)
    requires { depths d1 t1 ++ s1 = depths d2 t2 }
    variant { t1 }
    ensures { d1 >= d2 }
  = assert { depths d2 t2 = depths d2 t2 ++ Nil };
    match t1 with
    | Leaf -> ()
    | Node t3 t4 ->
        depths_subtree t3 t2 (d1+1) d2 (depths (d1+1) t4 ++ s1)
    end
68

69 70 71 72
  lemma depths_unique2:
    forall t1 t2: tree, d1 d2: int.
    depths d1 t1 = depths d2 t2 -> d1 = d2 && t1 = t2

73 74 75 76 77
end

module TreeReconstruction

  use export Tree
78 79
  use list.Length
  use list.HdTlNoOpt
80

81 82 83
  exception Failure
    (* used to signal the algorithm's failure i.e. there is no tree *)

84
  let rec build_rec (d: int) (s: list int) : (t: tree, s': list int)
85
    variant { length s, hd s - d }
86
    ensures { s = depths d t ++ s' }
87 88
    raises  { Failure -> forall t: tree, s' : list int. depths d t ++ s' <> s }
  = match s with
89 90 91 92 93
    | Nil ->
        raise Failure
    | Cons h t ->
        if h < d then raise Failure;
        if h = d then
94
          Leaf, t
95 96 97
        else
          let l, s = build_rec (d+1) s in
          let r, s = build_rec (d+1) s in
98
          Node l r, s
99 100
    end

101 102 103 104
  let build (s: list int) : tree
    ensures { depths 0 result = s }
    raises  { Failure -> forall t: tree. depths 0 t <> s }
  = let t, s = build_rec 0 s in
105 106 107 108 109 110 111 112 113
    match s with
    | Nil -> t
    | _ -> raise Failure
    end

end

module Harness

114
  use TreeReconstruction
115

116 117 118 119
  let harness ()
    ensures { result = Node Leaf (Node (Node Leaf Leaf) Leaf) }
    raises  { Failure -> false }
  = build (Cons 1 (Cons 3 (Cons 3 (Cons 2 Nil))))
120

121 122 123
  let harness2 ()
    ensures { false } raises { Failure -> true }
  = build (Cons 1 (Cons 3 (Cons 2 (Cons 2 Nil))))
124 125 126

end

127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143
(*
  A variant implementation proposed by Jayadev Misra

  Given the input list [x1; x2; ...; xn], we first turn it into the
  list of pairs [(x1, Leaf); (x2, Leaf); ...; (xn, Leaf)].  Then,
  repeatedly, we scan this list from left to right, looking for two
  consecutive pairs (v1, t1) and (v2, t2) with v1 = v2.  Then we
  replace them with the pair (v1-1, Node t1 t2) and we start again.
  We stop when there is only one pair left (v,t). Then we must have v=0.

  The implementation below achieves linear complexity using a zipper
  data structure to traverse the list of pairs. The left list contains
  the elements already traversed (thus on the left), in reverse order,
  and the right list contains the elements yet to be traversed.

*)

144 145 146 147 148
(* Proving termination is quite easy and we do it first (though we could,
   obviously, do it together with proving correctness) *)

module ZipperBasedTermination

149 150 151
  use Tree
  use list.Length
  use list.Reverse
152 153 154 155

  exception Failure

  let rec tc (left: list (int, tree)) (right: list (int, tree)) : tree
156
    variant { length left + length right, length right }
157
    raises  { Failure }
158
  = match left, right with
159 160 161 162 163 164 165 166 167 168 169 170 171 172 173
    | _, Nil ->
        raise Failure
    | Nil, Cons (v, t) Nil ->
        if v = 0 then t else raise Failure
    | Nil, Cons (v, t) right' ->
        tc (Cons (v, t) Nil) right'
    | Cons (v1, t1) left', Cons (v2, t2) right' ->
        if v1 = v2 then tc left' (Cons (v1 - 1, Node t1 t2) right')
        else tc (Cons (v2, t2) left) right'
    end

end

(* Now soundness and completeness *)

174 175
module ZipperBased

176 177 178
  use Tree
  use list.Length
  use list.Reverse
179

180 181 182
  (* the following function generalizes function [depths] to a forest, that
     is a list of pairs (depth, tree) *)

183 184 185 186 187
  function forest_depths (f: list (int, tree)) : list int = match f with
  | Nil -> Nil
  | Cons (d, t) r -> depths d t ++ forest_depths r
  end

188 189
  (* an obvious lemma on [forest_depths] *)

190 191 192 193
  lemma forest_depths_append:
    forall f1 f2: list (int, tree).
    forest_depths (f1 ++ f2) = forest_depths f1 ++ forest_depths f2

194 195 196
  (* to prove completeness, one needs an invariant over the list [left].
     The main ingredient is predicate [greedy] below, which states that
     [d] is distinct from all depths along the left branch of [d1, t1]. *)
197

198 199 200 201 202 203
  predicate greedy (d: int) (d1: int) (t1: tree) =
    d <> d1 /\ match t1 with Leaf -> true | Node l1 _ -> greedy d (d1+1) l1 end

  (* then we extend it to a list of pairs [(dn,tn); ...; (d2,t2); (d1,t1)]
     as follows: [greedy d2 d1 t1], [greedy d3 d2 t2], etc.
     this is inductive predicate [g] *)
204

205 206 207
  inductive g (l: list (int, tree)) =
    | Gnil: g Nil
    | Gone: forall d: int, t: tree. g (Cons (d, t) Nil)
208 209 210 211 212
    | Gtwo: forall d1 d2: int, t1 t2: tree, l: list (int, tree).
        greedy d1 d2 t2 -> g (Cons (d1, t1) l) ->
        g (Cons (d2, t2) (Cons (d1, t1) l))

  (* an easy lemma on [g] *)
213 214

  lemma g_append:
215
    forall l1 [@induction] l2: list (int, tree). g (l1 ++ l2) -> g l1
216

217 218 219 220 221 222
  (* key lemma for completeness: whenever we fail because [right] is empty,
     we have to prove that there is no solution

     Note: the proof first generalizes the statement as follows:
       forest_depths ((d1,t1) :: l) <> depths d t + s
     whenever d < d1 (see the corresponding Coq file) *)
223

224 225 226 227 228 229 230 231
  lemma depths_length: forall t d. length (depths d t) >= 1
  lemma forest_depths_length: forall l. length (forest_depths l) >= 0
  lemma g_tail: forall l1 l2: list (int, tree). g (l1 ++ l2) -> g l2

  lemma key_lemma : forall t l d d1 t1 s. d < d1 ->
    1 <= length l -> g (reverse (Cons (d1, t1) l)) ->
    not (forest_depths (Cons (d1, t1) l) = (depths d t) ++ s)

232 233
  lemma right_nil:
    forall l: list (int, tree). length l >= 2 -> g l ->
234 235 236 237 238
    forall t: tree, d: int.
    forest_depths (reverse l) <> depths d t

  (* key lemma for soundness: preservation of the invariant when we move
     a tree from [right] to [left] *)
239 240 241

  lemma main_lemma:
    forall l: list (int, tree), d1 d2: int, t1 t2: tree. d1 <> d2 ->
242 243 244 245 246 247 248 249 250 251 252
    g (Cons (d1, t1) l) ->
    match t2 with Node l2 _ -> greedy d1 (d2+1) l2 | Leaf -> true end ->
    g (Cons (d2, t2) (Cons (d1, t1) l))

  (* finally, we need a predicate to state that a forest [l] contains only
     leaves *)

  predicate only_leaf (l: list (int, tree)) = match l with
    | Nil -> true
    | Cons (_, t) r -> t = Leaf /\ only_leaf r
  end
253 254

  exception Failure
255

256 257
  let rec tc (left: list (int, tree)) (right: list (int, tree)) : tree
    requires { (* list [left] satisfies the invariant *)
258 259
      g left /\
      (* when [left] has one element, it can't be a solution *)
260 261
      match left with Cons (d1, _) Nil -> d1 <> 0 \/ right <> Nil
                    | _                -> true                    end /\
262 263 264
      (* apart (possibly) from its head, all elements in [right] are leaves;
         moreover the left branch of [right]'s head already satisfies
         invariant [g] when consed to [left] *)
265 266
      match right with
        | Cons (d2, t2) right' -> only_leaf right' /\
267
            match t2 with Node l2 _ -> g (Cons (d2+1, l2) left)
268
                        | Leaf      -> true end
269
        | Nil -> true end }
270
    variant { length left + 2 * length right }
271 272 273 274
    ensures { depths 0 result = forest_depths (reverse left ++ right) }
    raises { Failure ->
      forall t: tree. depths 0 t <> forest_depths (reverse left ++ right) }
  = match left, right with
275 276 277 278
    | _, Nil ->
        raise Failure
    | Nil, Cons (v, t) Nil ->
        if v = 0 then t else raise Failure
279 280
    | Nil, Cons (v, t) right' ->
        tc (Cons (v, t) Nil) right'
281 282 283 284 285
    | Cons (v1, t1) left', Cons (v2, t2) right' ->
        if v1 = v2 then tc left' (Cons (v1 - 1, Node t1 t2) right')
        else tc (Cons (v2, t2) left) right'
    end

286 287 288 289 290
  (* Getting function [build] from [tc] is easy: from the list
     [x1; x2; ...; xn] we simply build the list of pairs
     [(x1, Leaf); (x2, Leaf); ...; (xn, Leaf)].
     Function [map_leaf] below does this. *)

291 292 293 294 295
  let rec function map_leaf (l: list int) : list (int, tree) =
    match l with
    | Nil -> Nil
    | Cons d r -> Cons (d, Leaf) (map_leaf r)
    end
296

297 298
  (* two lemmas on [map_leaf] *)

299 300 301
  lemma map_leaf_depths:
    forall l: list int. forest_depths (map_leaf l) = l

302 303 304
  lemma map_leaf_only_leaf:
    forall l: list int. only_leaf (map_leaf l)

305 306 307 308
  let build (s: list int)
    ensures { depths 0 result = s }
    raises  { Failure -> forall t: tree. depths 0 t <> s }
  = tc Nil (map_leaf s)
309 310

end