Inital commit

2011-10-26 10:11:42 +02:00
commit c0da376199
888 changed files with 44367 additions and 0 deletions
@@ -0,0 +1,121 @@
+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