pqueue-test.mlw 1.04 KB
Newer Older
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
module Test

  use import list.List
  use import pqueue.Pqueue as P

  function v1 : elt
  function v2 : elt
  axiom values: rel v2 v1 /\ v1 <> v2

  let test0 () =
    let s = P.create () : P.t in
    assert { s.elts = Nil };
    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

module TestNoDup

  use import set.Fset
  use import pqueue.PqueueNoDup as P

  function v1 : elt
  function v2 : elt
  axiom values: rel v2 v1 /\ 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