mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
309be35d9c
- both Pqueue and PqueueNoDup now require a TotalPreOrder, not TotalOrder - Pqueue now modeled using sequences instead of lists - a harness module for Pqueue (external heapsort) - both Pqueue and PqueueNoDup now have coercions
58 lines
1.1 KiB
Plaintext
58 lines
1.1 KiB
Plaintext
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
|