1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
|
module Test
use seq.Seq
use import pqueue.Pqueue as P
val constant v1 : elt
val constant v2 : elt
axiom values: le v2 v1 /\ not (le v1 v2)
let test0 () =
let s = P.create () : P.t in
assert { s = empty };
let b = P.is_empty s in
assert { b = True };
let n = P.length s in
assert { n = 0 }
let test1 () =
raises { P.Empty }
let s = P.create () in
P.push v1 s;
let x = P.peek s in assert { x = v1 };
P.push v2 s;
assert { s == cons v2 (cons v1 empty) \/
s == cons v1 (cons v2 empty) };
let x = P.peek s in assert { x = v2 };
()
end
module TestNoDup
use set.Fset
use import pqueue.PqueueNoDup as P
val constant v1 : elt
val constant v2 : elt
axiom values: le v2 v1 /\ not (le v1 v2)
let test0 () =
let s = P.create () : P.t in
assert { s.elts = empty };
let b = P.is_empty s in
assert { b = True };
let n = P.length s in
assert { n = 0 }
let test1 () =
raises { P.Empty }
let s = P.create () in
P.push v1 s;
let x = P.peek s in assert { x = v1 };
P.push v2 s;
let x = P.peek s in assert { x = v2 };
()
end
|
