UNC-CH COMP 410
Priority Queue of int: Axiomatic definition
Operations
new : --> PQUE
insert : PQUE x int --> PQUE
getmin : PQUE --> ELT u err
delmin : PQUE --> PQUE
size : PQUE --> nat
empty : PQUE --> boolean
Behavior
size(new) = 0
size(insert(P,e)) = size(P) + 1
empty(new) = true
empty(insert(P,e)) = fals
getmin(new) = err
getmin(insert(P,e)) = if (empty(P))
then e
else if (e < getmin(P))
then e
else getmin(P)
(alternate way) getmin(insert(new,e)) = e
delmin(new) = new
delmin(insert(P,e)) = if (empty(P))
then New
else if (e < getmin(P))
then P
else insert(delmin(P),e)