## 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 int.Int type elt predicate le elt elt clone relations.TotalPreOrder with type t = elt, predicate rel = le, axiom . 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 constant 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 int.Int use bintree.Tree use export bintree.Size use export bintree.Occ type elt val predicate le elt elt clone relations.TotalPreOrder with type t = elt, predicate rel = le, axiom . (* [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 not (is_empty l) then root_is_min l; if not (is_empty r) then root_is_min r end let constant empty : tree elt = Empty ensures { heap result } ensures { size result = 0 } ensures { forall e. not (mem e result) } 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 array.Array use array.ArrayPermut use SkewHeaps clone export array.Sorted with type elt = elt, predicate le = le, axiom . use int.Int use ref.Ref use map.Occ as M use 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; label I in 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 (a.elts at 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.Heap": fully verified

Obligations | Alt-Ergo 2.3.0 |

VC for empty | 0.00 |

## Theory "skew_heaps.SkewHeaps": fully verified

Obligations | Alt-Ergo 2.0.0 | Alt-Ergo 2.3.1 | CVC4 1.7 | ||

VC for root_is_min | 0.65 | --- | --- | ||

VC for empty | 0.00 | --- | --- | ||

VC for get_min | --- | 0.00 | --- | ||

VC for merge | --- | --- | --- | ||

split_vc | |||||

variant decrease | --- | --- | 0.06 | ||

precondition | --- | --- | 0.04 | ||

variant decrease | --- | --- | 0.07 | ||

precondition | --- | --- | 0.04 | ||

postcondition | --- | --- | --- | ||

split_vc | |||||

postcondition | --- | --- | 0.03 | ||

postcondition | --- | --- | 0.04 | ||

postcondition | --- | --- | 0.04 | ||

postcondition | --- | 1.66 | --- | ||

postcondition | --- | --- | --- | ||

split_vc | |||||

postcondition | --- | --- | 0.05 | ||

postcondition | --- | --- | 0.03 | ||

postcondition | --- | --- | 0.04 | ||

postcondition | --- | --- | 0.06 | ||

postcondition | --- | --- | --- | ||

split_vc | |||||

postcondition | --- | --- | 0.04 | ||

postcondition | --- | --- | 0.03 | ||

postcondition | --- | --- | 0.04 | ||

postcondition | --- | --- | 0.07 | ||

VC for add | --- | 0.02 | --- | ||

VC for remove_min | --- | 0.02 | --- |

## Theory "skew_heaps.HeapSort": fully verified

Obligations | Alt-Ergo 2.3.1 | CVC4 1.5 | CVC4 1.7 | Z3 4.8.6 | |

VC for heapsort | --- | --- | --- | --- | |

split_goal_right | |||||

loop invariant init | 0.01 | --- | --- | --- | |

loop invariant init | 0.02 | --- | --- | --- | |

index in array bounds | 0.01 | --- | --- | --- | |

precondition | 0.01 | --- | --- | --- | |

assertion | 0.02 | --- | --- | --- | |

loop invariant preservation | 0.01 | --- | --- | --- | |

loop invariant preservation | 0.28 | --- | --- | --- | |

loop invariant init | 0.01 | --- | --- | --- | |

loop invariant init | 0.01 | --- | 0.07 | 0.04 | |

loop invariant init | 0.01 | --- | --- | --- | |

loop invariant init | 0.08 | --- | --- | --- | |

precondition | 0.01 | --- | --- | --- | |

index in array bounds | 0.02 | --- | --- | --- | |

precondition | 0.01 | --- | --- | --- | |

loop invariant preservation | --- | --- | --- | 0.11 | |

loop invariant preservation | 0.02 | --- | --- | --- | |

loop invariant preservation | --- | 0.10 | --- | --- | |

loop invariant preservation | --- | --- | --- | 0.06 | |

postcondition | 0.01 | --- | --- | --- | |

postcondition | 0.03 | --- | --- | --- | |

out of loop bounds | 0.01 | --- | --- | --- | |

out of loop bounds | 0.01 | --- | --- | --- |