Wiki Agenda Contact Version française

Computing the height of a tree in CPS style


Authors: Jean-Christophe Filliâtre / Andrei Paskevich

Topics: Trees

Tools: Why3

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



Computing the height of a tree in CPS style (author: Jean-Christophe FilliĆ¢tre)

module HeightCPS

  use import int.Int
  use import int.MinMax
  use import bintree.Tree
  use import bintree.Height
  use HighOrd

  function height_cps (t: tree 'a) (k: int -> 'b) : 'b =
    match t with
    | Empty -> k 0
    | Node l _ r ->
        height_cps l (\ hl.
        height_cps r (\ hr.
        k (1 + max hl hr)))
    end

  function height1 (t: tree 'a) : int = height_cps t (\ h. h)

  lemma height_cps_correct:
    forall t: tree 'a, k: int -> 'b. height_cps t k = k (height t)

  lemma height1_correct:
    forall t: tree 'a. height1 t = height t

end

with a while loop, manually obtained by compiling out recursion

module Iteration

  use import int.Int
  use import int.MinMax
  use import list.List
  use import bintree.Tree
  use import bintree.Size
  use import bintree.Height
  use import ref.Ref

  type cont 'a = Id | Kleft (tree 'a) (cont 'a) | Kright int (cont 'a)

  type what 'a = Argument (tree 'a) | Result int

  predicate is_id (k: cont 'a) =
    match k with Id -> true | _ -> false end

  predicate is_result (w: what 'a) =
    match w with Result _ -> true | _ -> false end

  function evalk (k: cont 'a) (r: int) : int =
    match k with
    | Id         -> r
    | Kleft  l k -> evalk k (1 + max (height l) r)
    | Kright x k -> evalk k (1 + max x r)
    end

  function evalw (w: what 'a) : int =
    match w with
    | Argument t -> height t
    | Result   x -> x
    end

  function sizek (k: cont 'a) : int =
    match k with
    | Id         -> 0
    | Kleft  t k -> 3 + 4 * size t + sizek k
    | Kright _ k -> 1 + sizek k
    end

  lemma sizek_nonneg: forall k: cont 'a. sizek k >= 0

  function sizew (w: what 'a) : int =
    match w with
    | Argument t -> 1 + 4 * size t
    | Result   _ -> 0
    end

  lemma helper1: forall t: tree 'a. 4 * size t >= 0
  lemma sizew_nonneg: forall w: what 'a. sizew w >= 0

  let height1 (t: tree 'a) : int
    ensures { result = height t }
  =
    let w = ref (Argument t) in
    let k = ref Id in
    while not (is_id !k && is_result !w) do
      invariant { evalk !k (evalw !w) = height t }
      variant   { sizek !k + sizew !w }
      match !w, !k with
      | Argument Empty,        _ -> w := Result 0
      | Argument (Node l _ r), _ -> w := Argument l; k := Kleft r !k
      | Result _, Id             -> absurd
      | Result v, Kleft r k0     -> w := Argument r; k := Kright v k0
      | Result v, Kright hl k0   -> w := Result (1 + max hl v); k := k0
      end
    done;
    match !w with Result r -> r | _ -> absurd end

end

Computing the height of a tree with an explicit stack (code: Andrei Paskevich / proof: Jean-Christophe FilliĆ¢tre)

module HeightStack

  use import int.Int
  use import int.MinMax
  use import list.List
  use import bintree.Tree
  use import bintree.Size
  use import bintree.Height

  type stack 'a = list (int, tree 'a)

  function heights (s: stack 'a) : int =
    match s with
    | Nil            -> 0
    | Cons (h, t) s' -> max (h + height t) (heights s')
    end

  function sizes (s: stack 'a) : int =
    match s with
    | Nil            -> 0
    | Cons (_, t) s' -> size t + sizes s'
    end

  lemma sizes_nonneg: forall s: stack 'a. sizes s >= 0

  let rec height_stack (m: int) (s: stack 'a) : int
    requires { m >= 0 }
    variant  { sizes s, s }
    ensures  { result = max m (heights s) }
  = match s with
    | Nil                     -> m
    | Cons (h, Empty) s'      -> height_stack (max m h) s'
    | Cons (h, Node l _ r) s' -> height_stack m (Cons (h+1,l) (Cons (h+1,r) s'))
   end

  let height1 (t: tree 'a) : int
    ensures { result = height t }
  = height_stack 0 (Cons (0, t) Nil)

end


download ZIP archive

Why3 Proof Results for Project "tree_height"

Theory "tree_height.HeightCPS": fully verified in 0.03 s

ObligationsAlt-Ergo (0.99.1)
height_cps_correct---
induction_ty_lex
  1.0.02
height1_correct0.01

Theory "tree_height.Iteration": fully verified in 0.89 s

ObligationsAlt-Ergo (0.99.1)Eprover (1.8-001)
sizek_nonneg------
induction_ty_lex
  1.0.01---
helper10.01---
sizew_nonneg---0.11
VC for height1------
split_goal_wp
  1. loop invariant init0.01---
2. loop invariant preservation0.02---
3. loop variant decrease0.01---
4. loop invariant preservation0.02---
5. loop variant decrease0.04---
6. unreachable point0.00---
7. loop invariant preservation0.02---
8. loop variant decrease0.02---
9. loop invariant preservation0.01---
10. loop variant decrease0.04---
11. loop invariant preservation0.01---
12. loop variant decrease0.02---
13. loop invariant preservation0.03---
14. loop variant decrease0.01---
15. loop invariant preservation0.02---
16. loop variant decrease0.04---
17. loop invariant preservation0.02---
18. loop variant decrease0.01---
19. postcondition0.05---
20. unreachable point0.02---
21. loop invariant preservation0.02---
22. loop variant decrease0.02---
23. loop invariant preservation0.02---
24. loop variant decrease0.02---
25. unreachable point0.01---
26. loop invariant preservation0.02---
27. loop variant decrease0.01---
28. loop invariant preservation0.02---
29. loop variant decrease0.02---
30. loop invariant preservation0.02---
31. loop variant decrease0.02---
32. loop invariant preservation0.02---
33. loop variant decrease0.02---
34. loop invariant preservation0.03---
35. loop variant decrease0.03---
36. loop invariant preservation0.02---
37. loop variant decrease0.02---

Theory "tree_height.HeightStack": fully verified in 0.47 s

ObligationsAlt-Ergo (0.99.1)CVC4 (1.4)Eprover (1.8-001)Vampire (0.6)
sizes_nonneg------------
induction_ty_lex
  1.------0.100.23
VC for height_stack------------
split_goal_wp
  1. postcondition0.01---------
2. variant decrease0.00---------
3. precondition0.02---------
4. postcondition---0.03------
5. variant decrease0.02---------
6. precondition0.00---------
7. postcondition---0.04------
VC for height1---0.02------