stdlib/queue.mlw

   1
   2 (** {1 Polymorphic mutable queues}
   3
   4     The module `Queue` below is mapped to OCaml's standard library
   5     module `Queue` by Why3's extraction.
   6
   7     Independently, a Why3 implementation of this module is also
   8     provided in `examples/queue_two_lists.mlw`.
   9 *)
  10
  11 module Queue
  12
  13   use seq.Seq
  14   use mach.peano.Peano
  15   use int.Int
  16
  17   type t 'a = abstract {
  18     mutable seq: Seq.seq 'a;
  19   }
  20
  21   meta coercion function seq
  22
  23   val create () : t 'a
  24     ensures { result = empty }
  25
  26   val push (x: 'a) (q: t 'a) : unit
  27     writes { q }
  28     ensures { q = snoc (old q) x }
  29
  30   exception Empty
  31
  32   val pop (q: t 'a) : 'a
  33     writes { q }
  34     ensures { old q <> empty }
  35     ensures { result = (old q)[0] }
  36     ensures { q = (old q)[1 ..] }
  37     raises  { Empty -> q = old q = empty }
  38
  39   val peek (q: t 'a) : 'a
  40     ensures { q <> empty }
  41     ensures { result = q[0] }
  42     raises  { Empty -> q = empty }
  43
  44   val safe_pop (q: t 'a) : 'a
  45     requires { q <> empty }
  46     writes { q }
  47     ensures { result = (old q)[0] }
  48     ensures { q = (old q)[1 ..] }
  49
  50   val safe_peek (q: t 'a) : 'a
  51     requires { q <> empty }
  52     ensures { result = q[0] }
  53
  54   val clear (q: t 'a) : unit
  55     writes  { q }
  56     ensures { q = empty }
  57
  58   val copy (q: t 'a) : t 'a
  59     ensures { result == q }
  60
  61   val is_empty (q: t 'a) : bool
  62     ensures { result <-> (q = empty) }
  63
  64   val length (q: t 'a) : Peano.t
  65     ensures { result = length q }
  66
  67   val transfer (q1 q2: t 'a) : unit
  68     writes  { q1, q2 }
  69     ensures { q1 = empty }
  70     ensures { q2 = (old q2) ++ (old q1) }
  71
  72 end
  73