Why3 Standard Library index

# Priority queues

## Polymorphic mutable priority queues

```module Pqueue

```

### Types

```  type elt
```

the abstract type of elements

```  predicate le elt elt
```

`elt` is equipped with a total pre order `le`

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

use int.Int
use seq.Seq
use seq.Occ

type t = abstract { mutable elts: seq elt }
invariant { forall i1 i2.
0 <= i1 <= i2 < length elts -> le elts[i1] elts[i2] }
meta coercion function elts
```

the priority queue is modeled as a sorted sequence of elements

### Operations

```  val create () : t ensures { result = empty }
```

create a fresh, empty queue

```  val push (x: elt) (q: t) : unit
writes  { q }
ensures { length q = 1 + length (old q) }
ensures { occ_all x q = 1 + occ_all x (old q) }
ensures { forall y. y <> x -> occ_all y q = occ_all y (old q) }
```

push an element in a queue

```  exception Empty
```

exception raised by `pop` and `peek` to signal an empty queue

```  val pop (q: t) : elt
writes {q}
ensures { length (old q) > 0 }
ensures { result = (old q)[0] }
ensures { q = (old q)[1..] }
raises  { Empty -> q = old q = empty }
```

remove and return the minimal element

```  val safe_pop (q: t) : elt
requires { length q > 0 }
writes   { q }
ensures  { result = (old q)[0] }
ensures  { q = (old q)[1..] }
```

remove and return the minimal element

```  val peek (q: t) : elt
ensures { length q > 0 }
ensures { result = q[0] }
raises  { Empty -> q = empty }
```

return the minimal element, without modifying the queue

```  val safe_peek (q: t) : elt
requires { length q > 0 }
ensures { result = q[0] }
```

return the minimal element, without modifying the queue

```  val clear (q: t) : unit
writes  { q }
ensures { q = empty }
```

empty the queue

```  val copy (q: t) : t
ensures { result == q }
```

return a fresh copy of the queue

```  val is_empty (q: t) : bool
ensures { result <-> q = empty }
```

check whether the queue is empty

```  val length (q: t) : int
ensures { result = length q }
```

return the number of elements in the queue

```end

module Harness
```

Test the interface above using an external heapsort

```  use int.Int
use array.Array
use array.IntArraySorted
use array.ArrayPermut
use map.Occ as MO
use seq.Seq
use seq.FreeMonoid
use seq.Occ as SO

clone Pqueue as PQ with type elt = int, predicate le = (<=)

let heapsort (a: array int) : unit
ensures { sorted a }
ensures { permut_all (old a) a }
= let n = length a in
let pq = PQ.create () in
for i = 0 to n - 1 do
invariant { length pq = i }
invariant { forall x. MO.occ x a.elts 0 n =
MO.occ x a.elts i n + SO.occ_all x pq }
PQ.push (Array.([]) a i) pq
done;
for i = 0 to n - 1 do
invariant { length pq = n - i }
invariant { sorted_sub a 0 i }
invariant { forall j k. 0 <= j < i -> 0 <= k < length pq ->
Array.([]) a j <= pq[k] }
invariant { forall x. MO.occ x (old a.elts) 0 n =
MO.occ x a.elts 0 i + SO.occ_all x pq }
a[i] <- PQ.safe_pop pq
done

end

```

## Simpler interface

when duplicate elements are not allowed

```module PqueueNoDup

```

### Types

```  type elt
```

the abstract type of elements

```  predicate le elt elt
```

`elt` is equipped with a total pre order `le`

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

use set.Fset

type t = abstract { mutable elts: fset elt }
```

the priority queue is modeled as a finite set of elements

```  meta coercion function elts

```

### Operations

```  val create () : t
ensures { result = empty }
```

create a fresh, empty queue

```  val push (x: elt) (q: t) : unit
writes  { q }
ensures { q = add x (old q) }
```

push an element in a queue

```  exception Empty
```

exception raised by `pop` and `peek` to signal an empty queue

```  predicate minimal_elt (x: elt) (s: fset elt) =
mem x s /\ forall e: elt. mem e s -> le x e
```

property of the element returned by `pop` and `peek`

```  val pop (q: t) : elt
writes  { q }
ensures { q = remove result (old q) }
ensures { minimal_elt result (old q) }
raises  { Empty -> q = old q = empty }
```

remove and returns the minimal element

```  val safe_pop (q: t) : elt
writes  { q }
requires { not q = empty }
ensures { q = remove result (old q) }
ensures { minimal_elt result (old q) }
```

remove and returns the minimal element

```  val peek (q: t) : elt
ensures { minimal_elt result q }
raises  { Empty -> q = empty }
```

return the minimal element, without modifying the queue

```  val safe_peek (q: t) : elt
requires { not q = empty }
ensures { minimal_elt result q }
```

return the minimal element, without modifying the queue

```  val clear (q: t) : unit
writes  { q }
ensures { q = empty }
```

empty the queue

```  val copy (q: t) : t
ensures { result = q }
```

return a fresh copy of the queue

```  val is_empty (q: t) : bool
ensures { result <-> q = empty }
```

check whether the queue is empty

```  val length (q: t) : int
ensures { result = cardinal q }
```

return the number of elements in the queue

```end
```

Generated by why3doc 1.5.0