## Queue implemented using two lists

Implementation of a mutable queue using two lists.

Authors: Léo Andrès

Topics: Data Structures

Tools: Why3

see also the index (by topic, by tool, by reference, by year)

Implementation of a mutable queue using two lists.

Author: Léo Andrès (Univ. paris-Sud)

```module Queue

use int.Int
use mach.peano.Peano
use list.List
use list.Length
use list.Reverse
use list.NthNoOpt
use list.Append
use seq.Seq
use seq.FreeMonoid

type t 'a = {
mutable front: list 'a; (* entry *)
mutable rear: list 'a;  (* exit *)
ghost mutable seq: Seq.seq 'a;
}
invariant { length seq = Length.length front + Length.length rear }
invariant { Length.length front > 0 -> Length.length rear > 0 }
invariant {
forall i. 0 <= i < length seq ->
seq[i] =
let n = Length.length rear in
if i < n then nth i rear
else nth (Length.length front - 1 - (i - n)) front }

meta coercion function seq

let create () : t 'a
ensures { result = empty }
= {
front = Nil;
rear = Nil;
seq = empty
}

let push (x: 'a) (q: t 'a) : unit
writes  { q }
ensures { q = snoc (old q) x }
= match q.front, q.rear with
| Nil, Nil -> q.rear <- Cons x Nil
| _        -> q.front <- Cons x q.front
end;
q.seq <- snoc q.seq x

let rec lemma nth_append (i: int) (l1: list 'a) (l2: list 'a)
requires { 0 <= i < Length.length l1 + Length.length l2 }
ensures {
nth i (Append.(++) l1 l2) =
if i < Length.length l1 then nth i l1
else nth (i - Length.length l1) l2 }
variant { l1 }
=
match l1 with
| Nil -> ()
| Cons _ r1 ->
if i > 0 then nth_append (i - 1) r1 l2
end

(* TODO: move this to stdlib ? *)
let rec lemma nth_rev (i: int) (l: list 'a)
requires { 0 <= i < Length.length l }
ensures { nth i l = nth (Length.length l - 1 - i) (reverse l) }
variant { l }
=
match l with
| Nil -> absurd
| Cons _ s ->
if i > 0 then nth_rev (i - 1) s
end

exception Empty

let pop (q: t 'a) : 'a
writes  { q }
ensures { (old q) <> empty }
ensures { result = (old q)[0] }
ensures { q = (old q)[1 ..] }
raises  { Empty -> q = old q = empty }
=
let res = match q.rear with
| Nil -> raise Empty
| Cons x Nil -> q.front, q.rear <- Nil, reverse q.front; x
| Cons x s -> q.rear <- s; x
end in
q.seq <- q.seq [1 ..];
res

let peek (q: t 'a) : 'a
ensures { q <> empty }
ensures { result = q[0] }
raises  { Empty -> q == empty }
=
match q.rear with
| Nil -> raise Empty
| Cons x _ -> x
end

let safe_pop (q: t 'a) : 'a
requires { q <> empty }
writes { q }
ensures { result = (old q)[0] }
ensures { q = (old q)[1 ..] }
= try pop q with Empty -> absurd end

let safe_peek (q: t 'a) : 'a
requires { q <> empty }
ensures { result = q[0] }
= try peek q with Empty -> absurd end

let clear (q: t 'a) : unit
writes { q }
ensures { q = empty }
=
q.seq <- empty;
q.rear <- Nil;
q.front <- Nil

let copy (q: t 'a) : t 'a
ensures { result == q }
= {
front = q.front;
rear = q.rear;
seq = q.seq
}

let is_empty (q: t 'a)
ensures { result <-> q == empty }
=
match q.front, q.rear with
| Nil, Nil -> true
| _ -> false
end

let length (q: t 'a) : Peano.t
ensures { result = Seq.length q.seq }
=
let rec length_aux (acc: Peano.t) (l: list 'a) : Peano.t
ensures { result = acc + Length.length l }
variant { l }
= match l with
| Nil -> acc
| Cons _ s -> length_aux (Peano.succ acc) s
end in
length_aux (length_aux Peano.zero q.front) q.rear

let transfer (q1: t 'a) (q2: t 'a) : unit
writes  { q1, q2 }
ensures { q1 = empty }
ensures { q2 = (old q2) ++ (old q1) }
= match q2.rear with
| Nil ->
q2.front, q2.rear, q2.seq <- q1.front, q1.rear, q1.seq
| _ ->
q2.front <- Append.(++) q1.front (Append.(++) (reverse q1.rear) q2.front);
q2.seq <- q2.seq ++ q1.seq;
end;
clear q1

end

module Correct
use Queue as Q
clone queue.Queue with
type t = Q.t, exception Empty = Q.Empty,
val create = Q.create, val push = Q.push, val pop = Q.pop, val peek = Q.peek,
val safe_pop = Q.safe_pop, val safe_peek = Q.safe_peek,
val clear = Q.clear, val copy = Q.copy, val is_empty = Q.is_empty,
val length = Q.length, val transfer = Q.transfer
end
```

the module above is a valid implementation of queue.Queue