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)