Algebraische Spezifikation

Stack

- types
Stack, t, Bool

- operators
createStack :: Stack
push        :: t -> Stack -> Stack
pop         :: Stack -> Stack
top         :: Stack -> t
isEmpty     :: Stack -> Bool

- axioms
s of type Stack, x of type t

isEmpty(createStack) = True
isEmpty(push x s) = False

top(push x s) = x
pop(push x s) = s

- preconditions
top: isEmpty s == False
pop: isEmpty s == False

Queue

- types
Queue, t, Bool

- operators
createQueue :: Queue
enqueue     :: t -> Queue -> Queue
dequeue     :: Queue -> Queue
first       :: Queue -> t
isEmpty     :: Queue -> Bool

- axioms
q of type Queue, x of type t

isEmpty(createQueue) = True
isEmpty(enqueue x q) = False

first(enqueue x createQueue) = x
first(enqueue x q) = first q

dequeue (enqueue x q) = enqueue x (dequeue q)

- preconditions
first : isEmpty q == False
dequeue: isEmpty q == False


Menge

- types
Set, t, Bool

- operators
createSet :: Set
insert    :: t -> Set -> Set
delete    :: t -> Set -> Set
isElement :: t -> Set -> Bool
isEmpty   :: Set -> Bool

- axioms
s of type Set, x,y of type t

isEmpty(createSet) = True
isEmpty(insert x s) = False

delete(createSet) = createSet
delete x (insert y s)
	| (x == y) = s
	| otherwise = insert y (delete x s)

isElement x (createSet) = False
isElement x (insert y s)
	| (x == y) = True
	| otherwise = isElement x s

- preconditions

Priority Queue

- types
PQueue, t, Bool

- operators
createPQueue :: PQueue
enqueue      :: t -> PQueue -> PQueue
dequeue      :: PQueue -> PQueue
min          :: PQueue -> t
isEmpty      :: PQueue -> Bool

- axioms
q of type PQueue, x of type t

isEmpty(createQueue) = True
isEmpty(enqueue x q) = False

min(enqueue x createPQueue) = x

dequeue(enqueue x createPQueue) = createPQueue

if (x < min q) then min(enqueue x q) = x
else min(enqueue x q) = min q

min(enqueue x q)
	| (x < min q) = x
	| otherwise = min q

dequeue(enqueue x q)
	| (x < min q) = q
	| otherwise = enqueue(x (dequeue q))

- preconditions
min : isEmpty q == False
dequeue: isEmpty q == False