vstte10_aqueue.mlw 1.5 KB
Newer Older
1 2 3 4
(*
   VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
   Problem 5: amortized queue

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

9 10
module AmortizedQueue

11 12 13
  use int.Int
  use option.Option
  use list.ListRich
14

15 16
  type queue 'a = { front: list 'a; lenf: int;
                    rear : list 'a; lenr: int; }
17
    invariant { length front = lenf >= length rear = lenr }
18
    by { front = Nil; lenf = 0; rear = Nil; lenr = 0 }
19

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

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

27
  let head (q: queue 'a) : 'a
28
    requires { sequence q <> Nil }
29
    ensures  { hd (sequence q) = Some result }
30
  = let Cons x _ = q.front in x
31

32
  let create (f: list 'a) (lf: int) (r: list 'a) (lr: int) : queue 'a
33
    requires { lf = length f /\ lr = length r }
34
    ensures  { sequence result = f ++ reverse r }
35 36
  = if lf >= lr then
      { front = f; lenf = lf; rear = r; lenr = lr }
37 38
    else
      let f = f ++ reverse r in
39
      { front = f; lenf = lf + lr; rear = Nil; lenr = 0 }
40

41
  let tail (q: queue 'a) : queue 'a
42
    requires { sequence q <> Nil }
43
    ensures  { tl (sequence q) = Some (sequence result) }
44 45
  = let Cons _ r = q.front in
    create r (q.lenf - 1) q.rear q.lenr
46

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

51
end