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 0.02 s
Obligations | Alt-Ergo (0.99.1) | CVC4 (1.4) | |
1. VC for root_is_min | --- | --- | |
split_goal_wp | |||
1. unreachable point | 0.02 | --- | |
2. variant decrease | 0.01 | --- | |
3. precondition | 0.01 | --- | |
4. variant decrease | 0.01 | --- | |
5. precondition | 0.01 | --- | |
6. postcondition | --- | 0.07 | |
7. postcondition | --- | 0.09 | |
8. variant decrease | 0.00 | --- | |
9. precondition | 0.01 | --- | |
10. postcondition | --- | 0.07 | |
11. postcondition | --- | 0.02 | |
2. VC for empty | 0.00 | --- | |
3. VC for is_empty | 0.01 | --- | |
4. VC for size | 0.01 | --- | |
5. VC for get_min | --- | --- | |
split_goal_wp | |||
1. unreachable point | 0.02 | --- | |
2. postcondition | 0.02 | --- | |
6. VC for merge | --- | --- | |
split_goal_wp | |||
1. postcondition | 0.01 | --- | |
2. postcondition | 0.01 | --- | |
3. postcondition | --- | 0.00 | |
4. postcondition | 0.04 | --- | |
5. postcondition | 0.00 | --- | |
6. postcondition | 0.01 | --- | |
7. postcondition | 0.01 | --- | |
8. postcondition | --- | 0.12 | |
9. postcondition | 0.03 | --- | |
10. variant decrease | 0.01 | --- | |
11. precondition | 0.01 | --- | |
12. postcondition | --- | 0.15 | |
13. postcondition | 0.01 | --- | |
14. postcondition | 0.02 | --- | |
15. variant decrease | 0.02 | --- | |
16. precondition | 0.01 | --- | |
17. postcondition | --- | 0.15 | |
18. postcondition | 0.01 | --- | |
19. postcondition | 0.01 | --- | |
7. VC for add | --- | --- | |
split_goal_wp | |||
1. precondition | 0.01 | --- | |
2. postcondition | 0.01 | --- | |
3. postcondition | 0.01 | --- | |
4. postcondition | 0.01 | --- | |
5. postcondition | 0.02 | --- | |
8. VC for remove_min | --- | --- | |
split_goal_wp | |||
1. unreachable point | 0.01 | --- | |
2. precondition | 0.01 | --- | |
3. postcondition | 0.01 | --- | |
4. postcondition | 0.01 | --- | |
5. postcondition | 0.07 | --- | |
6. postcondition | 0.02 | --- |
Theory "skew_heaps.HeapSort": fully verified in 0.00 s
Obligations | Alt-Ergo (0.99.1) | CVC4 (1.4) | |
1. VC for heapsort | --- | --- | |
split_goal_wp | |||
1. postcondition | 0.01 | --- | |
2. postcondition | 0.02 | --- | |
3. loop invariant init | 0.02 | --- | |
4. loop invariant init | 0.02 | --- | |
5. loop invariant init | 0.01 | --- | |
6. loop invariant init | 0.02 | --- | |
7. precondition | 0.01 | --- | |
8. type invariant | 0.00 | --- | |
9. index in array bounds | 0.02 | --- | |
10. precondition | 0.02 | --- | |
11. loop invariant preservation | 0.01 | --- | |
12. loop invariant preservation | 0.02 | --- | |
13. loop invariant preservation | 0.05 | --- | |
14. loop invariant preservation | 0.02 | --- | |
15. type invariant | 0.02 | --- | |
16. postcondition | 0.02 | --- | |
17. postcondition | 0.01 | --- | |
18. loop invariant init | 0.01 | --- | |
19. loop invariant init | 0.02 | --- | |
20. index in array bounds | 0.02 | --- | |
21. precondition | 0.01 | --- | |
22. assertion | --- | 0.63 | |
23. loop invariant preservation | 0.02 | --- | |
24. loop invariant preservation | --- | 1.40 | |
25. postcondition | 0.00 | --- | |
26. postcondition | 0.01 | --- | |
27. loop invariant init | 0.02 | --- | |
28. loop invariant init | 0.01 | --- | |
29. loop invariant init | 0.01 | --- | |
30. loop invariant init | 0.03 | --- | |
31. precondition | 0.02 | --- | |
32. type invariant | 0.02 | --- | |
33. index in array bounds | 0.01 | --- | |
34. precondition | 0.02 | --- | |
35. loop invariant preservation | 0.12 | --- | |
36. loop invariant preservation | 0.01 | --- | |
37. loop invariant preservation | 0.11 | --- | |
38. loop invariant preservation | 0.69 | --- | |
39. type invariant | 0.02 | --- | |
40. postcondition | 0.02 | --- | |
41. postcondition | 0.18 | --- |