Wiki Agenda Contact Version française

Skew heaps


Authors: Jean-Christophe Filliâtre

Topics: Data Structures

Tools: Why3

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



Skew heaps

Author: Jean-Christophe FilliĆ¢tre (CNRS)

module Heap

  use import int.Int

  type elt
  predicate le elt elt
  clone relations.TotalPreOrder with type t = elt, predicate rel = le

  type t

  function size t : int

  function occ elt t : int

  predicate mem (x: elt) (t: t) = occ x t > 0

  function minimum t : elt

  predicate is_minimum (x: elt) (t: t) =
    mem x t && forall e. mem e t -> le x e

  axiom min_is_min:
    forall t: t. 0 < size t -> is_minimum (minimum t) t

  val empty () : t
    ensures { size result = 0 }
    ensures { forall e. not (mem e result) }

  val size (t: t) : int
    ensures { result = size t }

  val is_empty (t: t) : bool
    ensures { result <-> size t = 0 }

  val get_min (t: t) : elt
    requires { 0 < size t }
    ensures  { result = minimum t }

  val merge (t1 t2: t) : t
    ensures  { forall e. occ e result = occ e t1 + occ e t2 }
    ensures  { size result = size t1 + size t2 }

  val add (x: elt) (t: t) : t
    ensures  { occ x result = occ x t + 1 }
    ensures  { forall e. e <> x -> occ e result = occ e t }
    ensures  { size result = size t + 1 }

  val remove_min (t: t) : t
    requires { 0 < size t }
    ensures  { occ (minimum t) result = occ (minimum t) t - 1 }
    ensures  { forall e. e <> minimum t -> occ e result = occ e t }
    ensures  { size result = size t - 1 }

end

module SkewHeaps

  use import int.Int
  use import bintree.Tree
  use export bintree.Size
  use export bintree.Occ

  type elt

  predicate le elt elt
  clone relations.TotalPreOrder with type t = elt, predicate rel = le

  (* [e] is no greater than the root of [t], if any *)
  predicate le_root (e: elt) (t: tree elt) = match t with
    | Empty      -> true
    | Node _ x _ -> le e x
  end

  (* [t] is a heap *)
  predicate heap (t: tree elt) = match t with
    | Empty      -> true
    | Node l x r -> le_root x l && heap l && le_root x r && heap r
  end

  function minimum (tree elt) : elt
  axiom minimum_def: forall l x r. minimum (Node l x r) = x

  predicate is_minimum (x: elt) (t: tree elt) =
    mem x t && forall e. mem e t -> le x e

  (* the root is the smallest element *)
  let rec lemma root_is_min (t: tree elt) : unit
     requires { heap t && 0 < size t }
     ensures  { is_minimum (minimum t) t }
     variant  { t }
  = match t with
    | Empty -> absurd
    | Node l _ r ->
        if l <> Empty then root_is_min l;
        if r <> Empty then root_is_min r
    end

  let empty () : tree elt
    ensures { heap result }
    ensures { size result = 0 }
    ensures { forall e. not (mem e result) }
  =
    Empty

  let is_empty (t: tree elt) : bool
    ensures { result <-> size t = 0 }
  =
    t = Empty

  let size (t: tree elt) : int
    ensures { result = size t }
  =
    size t

  let get_min (t: tree elt) : elt
    requires { heap t && 0 < size t }
    ensures  { result = minimum t }
  =
    match t with
      | Empty      -> absurd
      | Node _ x _ -> x
    end

  let rec merge (t1 t2: tree elt) : tree elt
    requires { heap t1 && heap t2 }
    ensures  { heap result }
    ensures  { forall e. occ e result = occ e t1 + occ e t2 }
    ensures  { size result = size t1 + size t2 }
    variant  { size t1 + size t2 }
  =
    match t1, t2 with
    | Empty, _ -> t2
    | _, Empty -> t1
    | Node l1 x1 r1, Node l2 x2 r2 ->
       if le x1 x2 then
         Node (merge r1 t2) x1 l1
       else
         Node (merge r2 t1) x2 l2
    end

  let add (x: elt) (t: tree elt) : tree elt
    requires { heap t }
    ensures  { heap result }
    ensures  { occ x result = occ x t + 1 }
    ensures  { forall e. e <> x -> occ e result = occ e t }
    ensures  { size result = size t + 1 }
  =
    merge (Node Empty x Empty) t

  let remove_min (t: tree elt) : tree elt
    requires { heap t && 0 < size t }
    ensures  { heap result }
    ensures  { occ (minimum t) result = occ (minimum t) t - 1 }
    ensures  { forall e. e <> minimum t -> occ e result = occ e t }
    ensures  { size result = size t - 1 }
  =
    match t with
      | Empty      -> absurd
      | Node l _ r -> merge l r
    end

end

(* application *)

module HeapSort

  use import SkewHeaps
  use import int.Int
  use import ref.Ref
  use import array.Array
  use import array.ArrayPermut
  clone export array.Sorted with type elt = elt, predicate le = le
  use import map.Occ as M
  use import bintree.Occ as H

  let heapsort (a: array elt) : unit
    ensures { sorted a }
    ensures { permut_all (old a) a }
  =
    let n = length a in
    let t = ref (empty ()) in
    for i = 0 to n - 1 do
      invariant { heap !t && size !t = i }
      invariant { forall e.
                  M.occ e a.elts i n + H.occ e !t = M.occ e a.elts 0 n }
      t := add a[i] !t;
      assert { M.occ a[i] a.elts i n = 1 + M.occ a[i] a.elts (i+1) n }
    done;
    'I:
    for i = 0 to n - 1 do
      invariant { sorted_sub a 0 i }
      invariant { heap !t && size !t = n - i }
      invariant { forall j. 0 <= j < i -> forall e. mem e !t -> le a[j] e }
      invariant { forall e.
                  M.occ e a.elts 0 i + H.occ e !t = M.occ e (at a.elts 'I) 0 n }
      a[i] <- get_min !t;
      t := remove_min !t
    done

end

download ZIP archive

Why3 Proof Results for Project "skew_heaps"

Theory "skew_heaps.SkewHeaps": fully verified in 1.20 s

ObligationsAlt-Ergo (0.99.1)CVC4 (1.4)
VC for root_is_min------
split_goal_wp
  1. unreachable point0.02---
2. variant decrease0.01---
3. precondition0.01---
4. variant decrease0.01---
5. precondition0.01---
6. postcondition---0.07
7. postcondition---0.09
8. variant decrease0.00---
9. precondition0.01---
10. postcondition---0.07
11. postcondition---0.02
VC for empty0.00---
VC for is_empty0.01---
VC for size0.01---
VC for get_min------
split_goal_wp
  1. unreachable point0.02---
2. postcondition0.02---
VC for merge------
split_goal_wp
  1. postcondition0.01---
2. postcondition0.01---
3. postcondition---0.00
4. postcondition0.04---
5. postcondition0.00---
6. postcondition0.01---
7. postcondition0.01---
8. postcondition---0.12
9. postcondition0.03---
10. variant decrease0.01---
11. precondition0.01---
12. postcondition---0.15
13. postcondition0.01---
14. postcondition0.02---
15. variant decrease0.02---
16. precondition0.01---
17. postcondition---0.15
18. postcondition0.01---
19. postcondition0.01---
VC for add------
split_goal_wp
  1. precondition0.01---
2. postcondition0.01---
3. postcondition0.01---
4. postcondition0.01---
5. postcondition0.02---
VC for remove_min------
split_goal_wp
  1. unreachable point0.01---
2. precondition0.01---
3. postcondition0.01---
4. postcondition0.01---
5. postcondition0.07---
6. postcondition0.02---

Theory "skew_heaps.HeapSort": fully verified in 7.31 s

ObligationsAlt-Ergo (0.99.1)CVC4 (1.4)
VC for heapsort------
split_goal_wp
  1. postcondition0.01---
2. postcondition0.02---
3. loop invariant init0.02---
4. loop invariant init0.02---
5. loop invariant init0.01---
6. loop invariant init0.02---
7. precondition0.01---
8. type invariant0.00---
9. index in array bounds0.02---
10. precondition0.02---
11. loop invariant preservation0.01---
12. loop invariant preservation0.02---
13. loop invariant preservation0.05---
14. loop invariant preservation0.02---
15. type invariant0.02---
16. postcondition0.02---
17. postcondition0.01---
18. loop invariant init0.01---
19. loop invariant init0.02---
20. index in array bounds0.02---
21. precondition0.01---
22. assertion---1.66
23. loop invariant preservation0.02---
24. loop invariant preservation---3.31
25. postcondition0.00---
26. postcondition0.01---
27. loop invariant init0.02---
28. loop invariant init0.01---
29. loop invariant init0.01---
30. loop invariant init0.03---
31. precondition0.02---
32. type invariant0.02---
33. index in array bounds0.01---
34. precondition0.02---
35. loop invariant preservation0.12---
36. loop invariant preservation0.01---
37. loop invariant preservation0.11---
38. loop invariant preservation1.35---
39. type invariant0.02---
40. postcondition0.02---
41. postcondition0.18---