queue.mlw 1.44 KB
Newer Older
1

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

module Queue

  use import list.List
  use import list.Append
8
  use import list.Length as L
9

10
  type t 'a model { mutable elts: list 'a }
11

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

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

  exception Empty

19 20 21 22
  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 }
23

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

29 30 31 32 33
  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 }

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
41
  val copy (q: t 'a) : t 'a ensures { result = q }
42

Andrei Paskevich's avatar
Andrei Paskevich committed
43
  val is_empty (q: t 'a) : bool
44
    ensures { result = True <-> q.elts = Nil }
45

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

Andrei Paskevich's avatar
Andrei Paskevich committed
48
  val length (q: t 'a) : int
49
    ensures { result = L.length q.elts }
50

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

56 57
end