pqueue.mlw 3.42 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3
(** {1 Priority queues} *)

(** {2 Polymorphic mutable priority queues} *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
4 5 6

module Pqueue

MARCHE Claude's avatar
MARCHE Claude committed
7 8
  (** {3 Types} *)

9
  type elt
10
  (** the abstract type of elements *)
11

12
  clone export relations.TotalOrder with type t = elt, axiom .
13
  (** `elt` is equipped with a total order `rel` *)
14

15 16 17 18
  use list.List
  use list.Mem
  use list.Permut
  use list.Length
19

20
  type t = abstract { mutable elts: list elt }
21
  (** the priority queue is modeled as a list of elements *)
22

MARCHE Claude's avatar
MARCHE Claude committed
23
  (** {3 Operations} *)
24

25
  val create () : t ensures { result.elts = Nil }
26
  (** create a fresh, empty queue *)
27

28 29
  val push (x: elt) (q: t) : unit writes {q}
    ensures { q.elts = Cons x (old q.elts) }
30
  (** push an element in a queue *)
31 32

  exception Empty
33
  (** exception raised by `pop` and `peek` to signal an empty queue *)
34 35 36

  predicate minimal_elt (x: elt) (s: list elt) =
     mem x s /\ forall e: elt. mem e s -> rel x e
37
  (** property of the element returned by `pop` and `peek` *)
38

39 40 41 42
  val pop (q: t) : elt writes {q}
    ensures { permut (Cons result q.elts) (old q.elts) }
    ensures { minimal_elt result (old q.elts) }
    raises  { Empty -> q.elts = (old q.elts) = Nil }
43
  (** remove and return the minimal element *)
44

Andrei Paskevich's avatar
Andrei Paskevich committed
45
  val peek (q: t) : elt
46 47
    ensures { minimal_elt result q.elts }
    raises  { Empty -> q.elts = Nil }
48
  (** return the minimal element, without modifying the queue *)
49

50
  val clear (q: t) : unit writes {q} ensures { q.elts = Nil }
51
  (** empty the queue *)
52

Andrei Paskevich's avatar
Andrei Paskevich committed
53
  val copy (q: t) : t ensures { result = q }
54
  (** return a fresh copy of the queue *)
55

Andrei Paskevich's avatar
Andrei Paskevich committed
56
  val is_empty (q: t) : bool
57
    ensures { result = True <-> q.elts = Nil }
58
  (** check whether the queue is empty *)
59

Andrei Paskevich's avatar
Andrei Paskevich committed
60
  val length (q: t) : int
61
    ensures { result = length q.elts }
62
  (** return the number of elements in the queue *)
63 64 65

end

MARCHE Claude's avatar
MARCHE Claude committed
66 67
(** {2 Simpler interface}

68
when duplicate elements are not allowed
MARCHE Claude's avatar
MARCHE Claude committed
69 70

*)
71 72 73

module PqueueNoDup

MARCHE Claude's avatar
MARCHE Claude committed
74
  (** {3 Types} *)
75

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
76
  type elt
77
  (** the abstract type of elements *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
78

79
  clone export relations.TotalOrder with type t = elt, axiom .
80
  (** `elt` is equipped with a total order `rel` *)
81

82
  use set.Fset
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
83

84
  type t = abstract { mutable elts: set elt }
85
  (** the priority queue is modeled as a finite set of elements *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
86

MARCHE Claude's avatar
MARCHE Claude committed
87
  (** {3 Operations} *)
88

89
  val create () : t ensures { result.elts = empty }
90
  (** create a fresh, empty queue *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
91

92 93
  val push (x: elt) (q: t) : unit writes {q}
    ensures { q.elts = add x (old q.elts) }
94
  (** push an element in a queue *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
95 96

  exception Empty
97
  (** exception raised by `pop` and `peek` to signal an empty queue *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
98

99 100
  predicate minimal_elt (x: elt) (s: set elt) =
     mem x s /\ forall e: elt. mem e s -> rel x e
101
  (** property of the element returned by `pop` and `peek` *)
102

103 104 105 106
  val pop (q: t) : elt writes {q}
    ensures { q.elts = remove result (old q.elts) }
    ensures { minimal_elt result (old q.elts) }
    raises  { Empty -> q.elts = (old q.elts) = empty }
107
  (** remove and returns the minimal element *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
108

Andrei Paskevich's avatar
Andrei Paskevich committed
109
  val peek (q: t) : elt
110 111
    ensures { minimal_elt result q.elts }
    raises  { Empty -> q.elts = empty }
112
  (** return the minimal element, without modifying the queue *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
113

114
  val clear (q: t) : unit writes {q} ensures {q.elts = empty }
115
  (** empty the queue *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
116

Andrei Paskevich's avatar
Andrei Paskevich committed
117
  val copy (q: t) : t ensures { result = q }
118
  (** return a fresh copy of the queue *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
119

Andrei Paskevich's avatar
Andrei Paskevich committed
120
  val is_empty (q: t) : bool
121
    ensures { result=True <-> q.elts = empty }
122
  (** check whether the queue is empty *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
123

Andrei Paskevich's avatar
Andrei Paskevich committed
124
  val length (q: t) : int
125
    ensures { result = cardinal q.elts }
126
  (** return the number of elements in the queue *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
127 128

end