Tilman
197 lines
5.3 KiB
Plaintext
197 lines
5.3 KiB
Plaintext
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 |