## 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 }
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
```

# 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.3.3 Alt-Ergo 2.4.2 CVC4 1.7 CVC5 1.0.5 VC for root_is_min --- 8.66 --- --- 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.01 postcondition --- --- --- --- split_vc postcondition --- --- 0.05 --- postcondition --- --- 0.03 --- postcondition --- --- 0.04 --- postcondition --- --- --- 0.04 postcondition --- --- --- --- split_vc postcondition --- --- 0.04 --- postcondition --- --- 0.03 --- postcondition --- --- 0.04 --- postcondition --- --- --- 0.05 VC for add 0.02 --- --- --- VC for remove_min 0.02 --- --- ---

## Theory "skew_heaps.HeapSort": fully verified

 Obligations Alt-Ergo 2.3.3 CVC4 1.5 CVC4 1.7 CVC4 1.8 Z3 4.12.2 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.19 --- --- --- --- loop invariant init 0.01 --- --- --- --- loop invariant init 0.01 --- 0.07 --- 0.02 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.25 loop invariant preservation 0.02 --- --- --- --- loop invariant preservation --- 0.10 --- --- --- loop invariant preservation --- --- --- 1.26 --- postcondition 0.01 --- --- --- --- postcondition 0.03 --- --- --- --- out of loop bounds 0.01 --- --- --- --- out of loop bounds 0.01 --- --- --- ---