examples/vstte10_aqueue.mlw

   1 (*
   2    VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
   3    Problem 5: amortized queue
   4
   5    Author: Jean-Christophe Filliatre (CNRS)
   6    Tool:   Why3 (see http://why3.lri.fr/)
   7 *)
   8
   9 module AmortizedQueue
  10
  11   use int.Int
  12   use option.Option
  13   use list.ListRich
  14
  15   type queue 'a = { front: list 'a; lenf: int;
  16                     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     q.front ++ reverse q.rear
  22
  23   let constant empty : queue 'a =
  24     { front = Nil; lenf = 0; rear = Nil; lenr = 0 }
  25     ensures { sequence result = Nil }
  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   = if lf >= lr then
  36       { front = f; lenf = lf; rear = r; lenr = lr }
  37     else
  38       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   = let Cons _ r = q.front in
  45     create r (q.lenf - 1) q.rear q.lenr
  46
  47   let enqueue (x: 'a) (q: queue 'a) : queue 'a
  48     ensures { sequence result = sequence q ++ Cons x Nil }
  49   = create q.front q.lenf (Cons x q.rear) (q.lenr + 1)
  50
  51 end