1b. mod. Menge 	(Haskell Listen)
2b. mod. Queue	(Haskell Listen)
3b. mod. Stack	(Haskell Listen)
4b. mod. Baum	(Haskell Listen)  // erstmal weggelassen

1c. mod. Menge	(Folgen)
2c. mod. Queue	(Folgen)
3c. mod. Stack	(Folgen)
4c. mod. Baum	(Folgen)

	
1b. Modellierende Spezifikation einer Menge	(Model,Spezifikation,Invariante)
---------------------------------------------------------------------------------------------------

Model :			Haskell Listen 

Invariante :	In einer Menge dürfen keine Duplikate vorkommen

Spezifikation:	createM :: [a]
				create 						= []
								
				isEmpty :: [a] -> Bool
				isEmpty [] 					= True
				isEmpty (x:xs)  			= False
				
				insert :: a -> [a] -> [a]
				insert x []					= [x]
				insert y (x:xs)				
							| y == x 		= (x:xs)
							| otherwise		= x:(insert y xs)
				
				delete :: a -> [a] -> [a]
				delete x []					= []
				delete y (x:xs)	
							| y == x 		= xs
							| otherwise		= x:(delete y xs)
				
				isIn :: a -> [a] -> Bool
				isIn x []					= False
				isIn y (x:xs)				
							| y == x 		= True
							| otherwise		= x:(isIn y xs)
							


2b. Modellierende Spezifikation einer Schlange	(Model,Spezifikation,Invariante)
---------------------------------------------------------------------------------------------------				
							
Modell:  Liste in Haskell [t]

Invariante :   length [t] <= MAX

Spezifikation:	createQ :: [t]
		createQ 					= []
					
		enqueue :: t -> [t] -> [t]
		enqueue x [] 					= [x]
		enqueue y (x:xs) 				= (x:xs) ++ [y]
					
		dequeue :: [t] -> [t]
		dequeue [] 					= error "Queue leer, Du OpfA"
		dequeue (x:xs) 					= xs 
								
		first :: [t] -> t
		first [] 					= error "Queue leer, Du OpfA"
		first (x:xs)  					= x
				
				
3b. Modellierende Spezifikation eines Stacks	(Model,Spezifikation,Invariante)
---------------------------------------------------------------------------------------------------				

Modell:  Liste in Haskell [t]

Invariante :   length [t] <= MAX

Spezifikation:	createS :: Stack s
				createS 				= []
				
				isEmpty :: Stack s -> Bool
				isEmpty []				= True
				isEmpty xs				= False
				
				push	:: e -> Stack s -> Stack s
				push x []				= [x]
				push y (x:xs)			= y : (x:xs)
								
				pop		:: Stack s -> Stack s
				pop []					= error "Stack ist leer"
				pop (x:xs)				= xs
							
				top		:: Stack s -> e
				top [] 					= error "Stack ist leer"
				top (x:xs)				= x	
				
				size	:: Stack s -> int
				size []					= 0
				size (x:xs)				= 1 + size (xs)
				


4b. Algebraische Spezifikation eines Baumes   	(Model,Spezifikation,Invariante)
--------------------------------------------------------------------------------------------------

									folgt
									
									

1c. Modellierende Spezifikation einer Menge		(Model,Spezifikation,Invariante)
---------------------------------------------------------------------------------------------------

Model : 			Menge = e | (xi)i=1..n , type xi = T , n <- N

Invariante : 		n < N && Alle (xi)i=1..n Exisitiert kein (xj)j=1..n mit xj = xi

Spezifikation :		createM = e 
					//post	return e
					
					isEmpty	Menge
					//post	if Menge == e return True else return False	
					
					//pre	createM && isIn T Menge = False (s. Invariante) && k < N
					insert	T Menge
					//post	insert T (xi)i=1..k => (xi)i=1..k+1 && xk+1 = T
					
					//pre 	createM
					delete	T (xi)i=1..k
					//post	(xi)i=1..k-1 && isIn T Menge = False
					
					//pre	createM
					isIn	T Menge
					//post	return ( Existiert ein (xi)i=1..k | xi == T )
					
					
				

2c. Modellierende Spezifikation einer Schlange	(Model,Spezifikation,Invariante)
---------------------------------------------------------------------------------------------------	

Model : 			Queue = e | (xi)i=1..n , type xi = T , n <- N

Invariante : 		n < N

Spezifikation :		createQ = e 
					//post	returns e
					
					isEmpty (xi)i=1..k
					//post 	if Queue == e  return True else return False 	
					
					//pre 	createQ && k < N
					enqueue	T Queue
					//post  enqueue	T (xi)i=1..k => (xi)i=1..k+1 && xk+1 = T
					
					//pre   !isEmpty
					dequeue	Queue
					//post	dequeue (xi)i=1..k   => (xi)i=2..k  (size = size-1)
					
					//pre	!isEmpty
					first	Queue
					//post	first (xi)i=1..k 	 => return x1
					



3c. Modellierende Spezifikation eines Stacks	(Model,Spezifikation,Invariante)
---------------------------------------------------------------------------------------------------

Model : 			Stack = e | (xi)i=1..n , type xi = T , n <- N

Invariante : 		n < N

Spezifikation :		createS = e 
					
					//pre 	createS
					isEmpty Stack 
					//post  Stack == e True else return False
					
					//pre 	createS && k < N
					push	T (xi)i=1..k-1 
					//post 	push T (xi)i=1..k-1 =>(xi)i=1..k && xk = T
					
					//pre	!isEmpty
					pop		(xi)i=1..n
					//pre	(xi)i=1..n-1
					
					//pre 	!isEmpty
					top		(xi)i=1..n
					//post	returns xn
					
					//pre 	createS
					size	(xi)i=1..n-1
					//post	returns n-1
				
				
4c. Algebraische Spezifikation eines Baumes   	(Model,Spezifikation,Invariante)
--------------------------------------------------------------------------------------------------

									folgt