Tilman
121 lines
2.1 KiB
Plaintext
121 lines
2.1 KiB
Plaintext
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 |