Beispiele - abstrakter Datentyp
Übersicht: Beispiele - abstrakter Datentyp
ADT : Warteschlange
In diesem Abschnitt werden wir anhand eines Beispiels auf Basis eines abstrakten Datentyps (ADT), neue Aspekte bezüglich des Formulierung von Eigenschaften mit QuickCheck aufzeigen.
Das Beispiel wird iterativ verfeinert und zu einer vollständigen Lösung entwickelt.
Als abstrakter Datentyp wird die Warteschlange bzw. Queue beschrieben und implementiert. Ausgehend von dieser Definition wird eine effizientere Implementierung entwickelt und die beiden Varianten bzgl. der Funktionaliätät verglichen.
Zum Thema "Die Formale Beschreibung abstrakter Datentypen" ein kurzer Exkurs:
ADT ist die "Beschreibung eines Datentyps vollständig durch die auf dem Datentyp definierten Operationen und deren Beziehungen untereinander
"Die Beschreibung besteht aus types, operations, preconditions und axioms.
Wobei unter types, die Aufzählung aller verwendeten ADT´s,
unter operations, der Aufzählung aller auf dem ADT definierten Operationen einschließlich Parametertypen und Resultattyp,
unter preconditions, den Vorbedingungen für die nur teilweise definierte Operationen,
und unter axioms, den Gesetze, die die Beziehungen zwischen den Operationen festlegen, verstanden werden.
01 types
02 Queue, Integer, Boolean
03
04 var
05 q, x:xq : Queue;
06 i : Integer;
07
08 operations
09 empty : --> Queue
10 add : Queue x Integer --> Queue
11 front : Queue --> Integer
12 remove : Queue --> Queue
13 isEmpty : Queue --> Boolean
14
15 preconditions
16 pre-remove(q) = not isEmpty(q)
17 pre-front(q) = not isEmpty(q)
18
19 axioms
20 isEmpty(empty()) = true
21 isEmpty(add(q,i)) = false
22 remove(add(x:xq,i)) = xq:i
23 front(add(x:xq,i)) = x
|
adt.def |
Codebeispiel 19
Implementierung 1 - Triviale Implementierung, Ausführbare Spezifikation
Aus der o.g. Definition des ADT Queue entwickeln wir die triviale Implementierung für die FIFO Queue und erhalten diese ausführbare Spezifikation. Die triviale Umsetzung der Warteschlange basiert auf einer Liste. Sie ist wie folgt definiert:
01 type Queue a = [a]
02 empty = []
03 add x q = q ++ [x]
04 isEmpty q = null q
05 front (x:q) = x
06 remove (x:q) = q
|
queue_dev.hs |
Codebeispiel 20
Folgende Laufzeitbetrachtungen zeigen die Schäche der Implementierung an:
T(empty), T(isEmpty), T(front), T(remove) => Const
T(empty), T(isEmpty), T(front), T(remove) = O(1)
T(add)(x q | n = length q) => O(n)
d.h. hier liegt lineares Wachstum vor(Zugriff auf alle Elemente einer Liste)
Damit ist die Funktion der add das Problem dieser Implementierung.
Implementierung 2 - Alternative, effiziente Implementierung
Die folgende alternative, effiziente Implementierung basiert auf zwei Listen. Die armoritisierte mittlere Laufzeit dieser Implemenzierung, ist nahezu konstant. Die Funktionen add und remove nutzen die Funktion flipQ. diese sorgt dafür, dass die Implentierungs internen Listen getauscht und entsprechend die Reihenfolge der Elemente umgedreht wird.
Die Funktion retrieve dient dazu, die implementierungsspezifischen Eigenschaften der QueueI an die Spezifaktion anzupassen, so dass beide Implementierungen verglichen werden können.
01 type QueueI a = ([a],[a])
02 emptyI = ([],[])
03 addI x (f,b) = flipQ (f,x:b)
04 isEmptyI (f,b) = null f
05 frontI (x:f,b) = x
06 removeI (x:f,b) = flipQ (f,b)
07 flipQ ([],b) = (reverse b,[])
08 flipQ q = q
09 retrieve :: QueueI Integer -> [Integer]
10 retrieve (f,b) = f ++ reverse b
|
queueI_dev.hs |
Codebeispiel 21
Zum besseren Verständnis der Implementierung der QueueI ist hier eine beispielhafte Auswertungsstrategie für addI gegeben:
I) q = ([],[])--> addI a q --> ([a],[])--> addI b q --> ([a],[b]) --> addI c q --> ([a],[c,b]) --> addI d q --> ([a],[d,c,b]) --> removeI q --> ([b,c,d],[])
II)([b,c,d],[]) --> removeI q --> ([c,d],[])
III)[b,c,d],[]) --> addI e q --> ([b,c,d],[e]) --> removeI() --> ([c,d][e])
Äquivalenz I - Implementierungen ADT: Queue
Um die alternative, effizientere Implementierung mit der Spezifikation zu vergleichen, formulieren wir wie folgt Eigenschaften unter Verwendung der im vorangegangenen Beispiel eingeführten retrieve Funktion.
01 -- Queue code - incorrect version (figures 2.2 and 2.3)
02
03 module Queue1 where
04 import QuickCheck
05
06 type Queue a = [a]
07 empty = []
08 add x q = q ++ [x]
09 isEmpty q = null q
10 front (x:q) = x
11 remove (x:q) = q
12
13 type QueueI a = ([a],[a])
14 emptyI = ([],[])
15 addI x (f,b) = (f,x:b)
16 isEmptyI (f,b) = null f
17 frontI (x:f,b) = x
18 removeI (x:f,b) = flipQ (f,b)
19 where
20 flipQ ([],b) = (reverse b,[])
21 flipQ q = q
22
23 retrieve :: QueueI Integer -> [Integer]
24 retrieve (f,b) = f ++ reverse b
25
26 prop_empty = retrieve emptyI == empty
27 prop_add x q = retrieve (addI x q) == add x (retrieve q)
28 prop_isEmpty q = isEmptyI q == isEmpty (retrieve q)
29 prop_front q = frontI q == front (retrieve q)
30 prop_remove q = retrieve (removeI q) == remove (retrieve q)
|
Queue1.hs |
Codebeispiel 22
Die Ausführung der Einzelnen Tests erzeugt folgende Ausgaben:
Queue1> quickCheck prop_empty
OK, passed 100 tests.
Queue1> quickCheck prop_add
OK, passed 100 tests.
Queue1> quickCheck prop_isEmpty
Falsifiable, after 6 tests:
([],[0])
Hier kommmt es zum Fehler! Das Problem liegt in der fehlenden Invarianten der Queue Repräsentation. Diese hatten wir bereits mit der Defintion des ADT gegeben: die fordere Liste der Warteschlange wird erst leer sein wenn die Hintere auch leer ist.
Äquivalenz II - Implementierungen - Verbesserung Formulierung der Eigenschaften
Wir verbesseren die Formulierung der Eigenschaften und führen die Invariante ein:
01 -- Queue code - corrected version (figures 2.4 and 2.5)
02
03 module Queue2 where
04 import QuickCheck
05
06 type Queue a = [a]
07 empty = []
08 add x q = q ++ [x]
09 isEmpty q = null q
10 front (x:q) = x
11 remove (x:q) = q
12
13 type QueueI a = ([a],[a])
14 emptyI = ([],[])
15 addI x (f,b) = flipQ (f,x:b)
16 isEmptyI (f,b) = null f
17 frontI (x:f,b) = x
18 removeI (x:f,b) = flipQ (f,b)
19
20 flipQ ([],b) = (reverse b,[])
21 flipQ q = q
22
23 retrieve :: QueueI Integer -> [Integer]
24 retrieve (f,b) = f ++ reverse b
25
26 invariant :: QueueI Integer -> Bool
27 invariant (f,b) = not (null f) || null b
28
29 prop_empty = retrieve emptyI == empty
30 prop_add x q = invariant q ==> retrieve (addI x q) == add x (retrieve q)
31 prop_isEmpty q = invariant q ==> isEmptyI q == isEmpty (retrieve q)
32 prop_front q = invariant q ==> frontI q == front (retrieve q)
33 prop_remove q = invariant q ==> retrieve (removeI q) == remove (retrieve q)
34
35 prop_inv_empty = invariant emptyI
36 prop_inv_add x q = invariant q ==> invariant (addI x q)
37 prop_inv_remove q = invariant q && not (isEmptyI q) ==> invariant (removeI q)
|
Queue2.hs |
Codebeispiel 23
Aus der gegebenen Definition der Invarianten ist ersichtlich, nur wenn der zweite Teil der Queue leer ist, ist auch der erste Teil leer!
invariant :: QueueI Integer -> Bool
invariant (f,b) = not (null f) || null b
Die erneute Ausführung der einzelnen Tests erzeugt folgende Ausgaben:
Queue2> quickCheck prop_empty
OK, passed 100 tests.
Queue2> quickCheck prop_add
OK, passed 100 tests.
Queue2> quickCheck prop_isEmpty
OK, passed 100 tests.
Queue2> quickCheck prop_front
1
Program error: {frontI ([],[])}
Es kommt erneut zum Fehler. quickCheck prop_front führt zum Fehler. Die Meldung macht die Ursache sichtbar: Es kommt zum Fehler, wenn aus einer leeren Warteschlange front gesagt wird. Es muss über eine Vorbedingung sichergestellt werden, dass die Warteschlange nicht leer ist.
Ergebnis der iterativen Verfeinerung
Wir verbesseren die Formulierung der Eigenschaften und führen die Vorbedingung ein:
Jetzt haben wir eine präzise Formulierung aller notwendigen Eigenschaften um die Warteschlange zu beschreiben.
01 -- Queue code - corrected version (figures 2.4 and 2.5)
02
03 module Queue2 where
04 import QuickCheck
05
06 type Queue a = [a]
07 empty = []
08 add x q = q ++ [x]
09 isEmpty q = null q
10 front (x:q) = x
11 remove (x:q) = q
12
13 type QueueI a = ([a],[a])
14 emptyI = ([],[])
15 addI x (f,b) = flipQ (f,x:b)
16 isEmptyI (f,b) = null f
17 frontI (x:f,b) = x
18 removeI (x:f,b) = flipQ (f,b)
19
20 flipQ ([],b) = (reverse b,[])
21 flipQ q = q
22
23 retrieve :: QueueI Integer -> [Integer]
24 retrieve (f,b) = f ++ reverse b
25
26 invariant :: QueueI Integer -> Bool
27 invariant (f,b) = not (null f) || null b
28
29 prop_empty = retrieve emptyI == empty
30 prop_add x q = invariant q ==> retrieve (addI x q) == add x (retrieve q)
31 prop_isEmpty q = invariant q ==> isEmptyI q == isEmpty (retrieve q)
32 prop_front q = invariant q && not (isEmptyI q) ==>
33 frontI q == front (retrieve q)
34 prop_remove q = invariant q && not (isEmptyI q) ==>
35 retrieve (removeI q) == remove (retrieve q)
36
37 prop_inv_empty = invariant emptyI
38 prop_inv_add x q = invariant q ==> invariant (addI x q)
39 prop_inv_remove q = invariant q && not (isEmptyI q) ==> invariant (removeI q)
|
Queue2.1.hs |
Codebeispiel 24
Die Zeilen 31 und 34 mit den Eigenschaften prop_front q und prop_remove q sind um die Vorbedingung not (isEmptyI q) ==> ergänzt.
Damit ist die die Spezifikation und die Dokumentation erheblich bereichert worden.
Es sind alle zu berücksichtigenden Bedingungen in die Eigenschaften bzw. die Implementierung eingeflossen.
Die abschliessenden Tests erzeugen folgende Ergebnisse:
Queue2> quickCheck prop_empty
OK, passed 100 tests.
Queue2> quickCheck prop_add
OK, passed 100 tests.
Queue2> quickCheck prop_isEmpty
OK, passed 100 tests.
Queue2> quickCheck prop_front
OK, passed 100 tests.
Queue2> quickCheck prop_remove
OK, passed 100 tests.
Queue2> quickCheck prop_inv_empty
OK, passed 100 tests.
Alle Test sind erfolgreich!
Formulierung mathematischer Eigenschaften
Die u.g. Gleichungen bieten eine komplette Spezifikation der Queue Operationen.
Dabei erlauben sie das Ausdrücken von Queues in der Form :
addI x1 (addI x2 ... ( addI xk emptyI))
01 prop_isEmpty q = invariant q ==> isEmptyI q == (q == emptyI)
02 prop_front_empty x = frontI (addI x emptyI) == x
03 prop_front_add x q = invariant q && not (isEmptyI q) ==> frontI (addI x q) == frontI q
04 prop_remove_empty x = removeI (addI x emptyI) == emptyI
05 prop_remove_add x q = invariant q && not (isEmptyI q) ==> removeI (addI x q) == addI x (removeI q
|
math_queue.hs |
Codebeispiel 25
Die folgende komplette Darstellung, ist der Ausagngspunkt für die notwendigen Test.
01 -- Queue code - incorrect algebraic specification (figure 2.6)
02
03 module Queue3 where
04 import QuickCheck
05
06 type QueueI a = ([a],[a])
07 emptyI = ([],[])
08 addI x (f,b) = flipQ (f,x:b)
09 isEmptyI (f,b) = null f
10 frontI (x:f,b) = x
11 removeI (x:f,b) = flipQ (f,b)
12
13 flipQ ([],b) = (reverse b,[])
14 flipQ q = q
15
16 invariant :: QueueI Integer -> Bool
17 invariant (f,b) = not (null f) || null b
18
19 prop_isEmpty q = invariant q ==> isEmptyI q == (q == emptyI)
20
21 prop_front_empty :: Integer -> Bool
22 prop_front_empty x = frontI (addI x emptyI) == x
23
24 prop_front_add x q = invariant q && not (isEmptyI q) ==>
25 frontI (addI x q) == frontI q
26
27 prop_remove_empty :: Integer -> Bool
28 prop_remove_empty x = removeI (addI x emptyI) == emptyI
29
30 prop_remove_add :: Integer -> QueueI Integer -> Property
31 prop_remove_add x q = invariant q && not (isEmptyI q) ==>
32 removeI (addI x q) == addI x (removeI q)
33
34 retrieve :: QueueI Integer -> [Integer]
35 retrieve (f,b) = f ++ reverse b
36
37 q `equiv` q´ = invariant q && invariant q´ && retrieve q == retrieve q´
38
39 prop_isEmpty_equiv q =
40 invariant q && isEmptyI q ==>
41 isEmptyI q == (q `equiv` emptyI)
42
|
Queue3.hs |
Codebeispiel 26
Mit diesem Beispiel sollen möglichen Unterschiedliche Ansätze, ADT (bzw. Referenzimplmentierungen) und Mathematische Notation, für die Formulierung von Eigenschaften vergleichend nebeneinandergestellt werden.
Man betrachte hier folgende Eigenschaften
retrieve emptyI == empty <==>(vgl.) isEmptyI q == (q == emptyI)
prop_isEmpty q = invariant q => retrieve emptyI == empty <==> prop_isEmpty q = invariant q ==> isEmptyI q == (q == emptyI)
Die Ausführung der Test erzeugt folgende Ergebnisse:
Queue3> quickCheck prop_isEmpty
OK, passed 100 tests.
Queue3> quickCheck prop_front_empty
OK, passed 100 tests.
Queue3> quickCheck prop_remove_empty
OK, passed 100 tests.
Queue3> quickCheck prop_front_add
OK, passed 100 tests.
Queue3> quickCheck prop_remove_add
Falsifiable, after 1 tests: [n]
0
([-2],[2])
Hier kommt es zum Fehler, da die beiden Seiten die gleiche Queue (sind äquivalent) repräsentieren aber nicht gleich sind!
Folgende Betrachtung als Veranschaulichung:
linke Seite: [removeI (addI x q)] --> [([x,y],[])] <==> Rechte Seite: [addI x (removeI q)] --> [([x],[y])]
mit der einführung des `equiv` Operators in folegender Form:
q `equiv` q´ = invariant q && invariant q´ && retrieve q == retrieve q
kann diese unpräzise Definition korrigiert werden, so dass die noch ausstehenden Tests erfolgen können.
Die Ausführung der Test erzeugt folgende Ergebnisse:
Queue3> quickCheck prop_isEmpty_equiv
Arguments exhausted after 69 tests.
Durch das Quantifizieren über alle Queue´s q und q´ und die Auswahl von 2 beliebigen Listen werden die von QuickCheck generieren unpassenden Kombinationen / Testfälle verworfen. Dies ist ineffizient, da sehr selten die Bedingungen erfüllt werden.
Die Beispiele zu insertOrdered und die vorangegangene Variante der Queue sind Beispiele für die Formulierung von Eigenschaft auf Basis von Referenzimplementierungen. Das erste Beispiel mit der Assoziativität des (+) Operators ist ein Beispeil für die mathematische Formulierung von Eigenschaften. Der Vergleich der Beiden Ansätze zeigt, dass mit Hilfe der mathematischen Formulierung der Eigenschaft mathematisch korrekte und sehr genau spezifiziert werden kann. Die Formulierungen häufig aber ungeeignet für Test sind, wie es das letzte Beispiel zeigt.
Code generated with AusarbeitungGenerator Version 1.1, weblink