## Amortized Queue, in Why3

Queue with good amortized complexity using linked lists, Why3 version

Authors: Jean-Christophe Filliâtre

Tools: Why3

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

```(*
VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
Problem 5: amortized queue

Author: Jean-Christophe Filliatre (CNRS)
Tool:   Why3 (see http://why3.lri.fr/)
*)

module AmortizedQueue

use import int.Int
use import option.Option
use import list.ListRich

type queue 'a = { front: list 'a; lenf: int;
rear : list 'a; lenr: int; }
invariant { length self.front = self.lenf >= length self.rear = self.lenr }

function sequence (q: queue 'a) : list 'a =
q.front ++ reverse q.rear

let empty () ensures { sequence result = Nil }
= { front = Nil; lenf = 0; rear = Nil; lenr = 0 } : queue 'a

requires { sequence q <> Nil }
ensures { hd (sequence q) = Some result }
= match q.front with
| Nil      -> absurd
| Cons x _ -> x
end

let create (f: list 'a) (lf: int) (r: list 'a) (lr: int)
requires { lf = length f /\ lr = length r }
ensures { sequence result = f ++ reverse r }
= if lf >= lr then
{ front = f; lenf = lf; rear = r; lenr = lr }
else
let f = f ++ reverse r in
{ front = f; lenf = lf + lr; rear = Nil; lenr = 0 }

let tail (q: queue 'a)
requires { sequence q <> Nil }
ensures { tl (sequence q) = Some (sequence result) }
= match q.front with
| Nil      -> absurd
| Cons _ r -> create r (q.lenf - 1) q.rear q.lenr
end

let enqueue (x: 'a) (q: queue 'a)
ensures { sequence result = sequence q ++ Cons x Nil }
= create q.front q.lenf (Cons x q.rear) (q.lenr + 1)

end
```