Why3 Standard Library index

# Priority queues

## Polymorphic mutable priority queues

```module Pqueue

```

### Types

```  type elt
```

the abstract type of elements

```  clone export relations.TotalOrder with type t = elt
```

`elt` is equipped with a total order `rel`

```  use import list.List
use import list.Mem
use import list.Permut
use import list.Length

type t model { mutable elts: list elt }
```

the priority queue is modeled as a list of elements

### Operations

```  val create () : t ensures { result.elts = Nil }
```

create a fresh, empty queue

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

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: list elt) =
mem x s /\ forall e: elt. mem e s -> rel x e
```

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

```  val pop (q: t) : elt writes {q}
ensures { permut (Cons result q.elts) (old q.elts) }
ensures { minimal_elt result (old q.elts) }
raises  { Empty -> q.elts = (old q.elts) = Nil }
```

remove and return the minimal element

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

return the minimal element, without modifying the queue

```  val clear (q: t) : unit writes {q} ensures { q.elts = Nil }
```

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 = True <-> q.elts = Nil }
```

check whether the queue is empty

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

return the number of elements in the queue

```end

```

## Simpler interface

when duplicate elements are not allowed

```module PqueueNoDup

```

### Types

```  type elt
```

the abstract type of elements

```  clone export relations.TotalOrder with type t = elt
```

`elt` is equipped with a total order `rel`

```  use import set.Fset

type t model { mutable elts: set elt }
```

the priority queue is modeled as a finite set of elements

### Operations

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

create a fresh, empty queue

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

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: set elt) =
mem x s /\ forall e: elt. mem e s -> rel x e
```

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

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

remove and returns the minimal element

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

return the minimal element, without modifying the queue

```  val clear (q: t) : unit writes {q} ensures {q.elts = 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=True <-> q.elts = empty }
```

check whether the queue is empty

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

return the number of elements in the queue

```end
```

Generated by why3doc 0.87.3