queue.mlw 1.45 KB
Newer Older
1

MARCHE Claude's avatar
MARCHE Claude committed
2
(** {1 Polymorphic mutable queues} *)
3 4 5

module Queue

6
  use mach.peano.Peano
7 8 9
  use list.List
  use list.Append
  use list.Length as L
10

11
  type t 'a = abstract { mutable elts: list 'a }
12

13
  val create () : t 'a ensures { result.elts = Nil }
14

15 16
  val push (x: 'a) (q: t 'a) : unit writes {q}
    ensures { q.elts = old q.elts ++ Cons x Nil }
17 18 19

  exception Empty

20 21 22 23
  val pop (q: t 'a) : 'a writes {q}
    ensures { match old q.elts with Nil -> false
      | Cons x t -> result = x /\ q.elts = t end }
    raises  { Empty -> q.elts = old q.elts = Nil }
24

25
  val peek (q: t 'a) : 'a
26 27 28
    ensures { match q.elts with Nil -> false
      | Cons x _ -> result = x end }
    raises  { Empty -> q.elts = Nil }
29

30 31 32 33 34
  val safe_pop (q: t 'a) : 'a writes {q}
    requires { q.elts <> Nil }
    ensures { match old q.elts with Nil -> false
      | Cons x t -> result = x /\ q.elts = t end }

35
  val safe_peek (q: t 'a) : 'a
36 37 38 39
    requires { q.elts <> Nil }
    ensures { match q.elts with Nil -> false
      | Cons x _ -> result = x end }

40
  val clear (q: t 'a) : unit writes {q} ensures { q.elts = Nil }
41

42
  val copy (q: t 'a) : t 'a ensures { result = q }
43

44
  val is_empty (q: t 'a) : bool
45
    ensures { result = True <-> q.elts = Nil }
46

47 48
  function length (q: t 'a) : int = L.length q.elts

49
  val length (q: t 'a) : Peano.t
50
    ensures { result = L.length q.elts }
51

52 53 54 55 56
  val transfer (q1 q2: t 'a) : unit
    writes  { q1, q2 }
    ensures { q1.elts = Nil }
    ensures { q2.elts = old q2.elts ++ old q1.elts }

57 58
end