On functional logic programming and its application to testing [Elektronische Ressource] / Sebastian Fischer

Sujets

• Informatik

Informations

• Publié par: christian-albrechts-universitat_zu_kiel
• Publié le: 01 janvier 2010
• Nombre de lectures: 15
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

On Functional Logic Programming
and its Application to Testing
Dissertation
zur Erlangung des akademischen Grades
Doktor der Naturwissenschaften
(Dr. rer. nat.)
der Technischen Fakultät
der Christian-Albrechts-Universität zu Kiel
Sebastian Fischer
Kiel, 20101. Gutachter Prof. Dr. Michael Hanus
2. Gutachter Prof. Dr. Herbert Kuchen
3. Gutachter Priv.-Doz. Dr. Frank Huch
Datum der mündlichen Prüfung 27. Mai 2010
iiIn Deiner Sprache saßen andere Augen.
Klavki, †2009
iiiivContents
1 Introduction 1
1.1 Syntax of programs . . . . . . . . . . . . . . . . . . . . . . . 1
1.2 Organisational remarks . . . . . . . . . . . . . . . . . . . . . 4
2 Declarative Programming 5
2.1 Functional programming . . . . . . . . . . . . . . . . . . . . 6
2.1.1 Type polymorphism and higher-order functions . . . . 7
2.1.2 Lazy evaluation . . . . . . . . . . . . . . . . . . . . . 9
2.1.3 Class-based overloading . . . . . . . . . . . . . . . . 11
2.1.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . 19
2.2 Functional logic programming . . . . . . . . . . . . . . . . . 19
2.2.1 Logic variables . . . . . . . . . . . . . . . . . . . . . 20
2.2.2 Nondeterminism . . . . . . . . . . . . . . . . . . . . 21
2.2.3 Lazy nondeterminism . . . . . . . . . . . . . . . . . . 23
2.2.4 Call-time choice . . . . . . . . . . . . . . . . . . . . . 25
2.2.5 Search . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2.2.6 Constraints . . . . . . . . . . . . . . . . . . . . . . . 31
2.2.7 Summary . . . . . . . . . . . . . . . . . . . . . . . . 34
2.3 Chapter notes . . . . . . . . . . . . . . . . . . . . . . . . . . 34
3 Generating Tests 35
3.1 Black-box testing . . . . . . . . . . . . . . . . . . . . . . . . 35
3.1.1 Property-based testing . . . . . . . . . . . . . . . . . 36
3.1.2 Defining test-case generators . . . . . . . . . . . . . . 38
3.1.3 Enumerating test cases . . . . . . . . . . . . . . . . . 42
3.1.4 Experiments . . . . . . . . . . . . . . . . . . . . . . . 51
3.1.5 Implementation . . . . . . . . . . . . . . . . . . . . . 57
3.1.6 Summary . . . . . . . . . . . . . . . . . . . . . . . . 59
3.2 Glass-box testing . . . . . . . . . . . . . . . . . . . . . . . . 60
3.2.1 Demand-driven testing . . . . . . . . . . . . . . . . . 61
3.2.2 Fair predicates . . . . . . . . . . . . . . . . . . . . . . 67
3.2.3 Practical experiments . . . . . . . . . . . . . . . . . . 70
3.2.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . 75
3.3 Chapter notes . . . . . . . . . . . . . . . . . . . . . . . . . . 76
vContents
4 Code Coverage 79
4.1 Control flow . . . . . . . . . . . . . . . . . . . . . . . . . . . 81
4.1.1 Rule coverage . . . . . . . . . . . . . . . . . . . . . . 82
4.1.2 Call coverage . . . . . . . . . . . . . . . . . . . . . . 82
4.2 Data flow . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
4.2.1 Constructors flow to patterns . . . . . . . . . . . . . . 85
4.2.2 Functions flow to applications . . . . . . . . . . . . . 86
4.2.3 Comparison with Control Flow . . . . . . . . . . . . . 87
4.3 Monitoring code coverage . . . . . . . . . . . . . . . . . . . 88
4.3.1 Lazy coverage collection . . . . . . . . . . . . . . . . 88
4.3.2 Combinators for coverage collection . . . . . . . . . . 91
4.3.3 Formalisation of program transformation . . . . . . . 96
4.3.4 Implementation of coverage combinators . . . . . . . 100
4.4 Experimental evaluation . . . . . . . . . . . . . . . . . . . . 103
4.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108
4.6 Chapter notes . . . . . . . . . . . . . . . . . . . . . . . . . . 109
5 Explicit Nondeterminism 111
5.1 Nondeterminism monads . . . . . . . . . . . . . . . . . . . . 111
5.1.1 Laws . . . . . . . . . . . . . . . . . . . . . . . . . . . 112
5.1.2 Backtracking . . . . . . . . . . . . . . . . . . . . . . 113
5.1.3 Fair search . . . . . . . . . . . . . . . . . . . . . . . . 120
5.1.4 Experiments . . . . . . . . . . . . . . . . . . . . . . . 123
5.1.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . 126
5.2 Combining laziness with nondeterminism . . . . . . . . . . . 127
5.2.1 Explicit sharing . . . . . . . . . . . . . . . . . . . . . 128
5.2.2 Intuitions of explicit sharing . . . . . . . . . . . . . . 132
5.2.3 Laws of explicit sharing . . . . . . . . . . . . . . . . . 135
5.2.4 Implementing explicit sharing . . . . . . . . . . . . . 140
5.2.5 Generalised, efficient implementation . . . . . . . . . 146
5.2.6 Summary . . . . . . . . . . . . . . . . . . . . . . . . 153
5.3 Chapter notes . . . . . . . . . . . . . . . . . . . . . . . . . . 154
6 Conclusions 157
6.1 Declarative programming promotes concepts that increase
the potential for abstraction. . . . . . . . . . . . . . . . . . . 158
6.2 The mechanism to execute functional logic programs is tailor
made for generating tests. . . . . . . . . . . . . . . . . . . . . 159
6.3 Declarative programs call for new notions of code coverage. . 162
6.4 Lazy nondeterministic programs can be turned into equiva-
lent purely functional programs. . . . . . . . . . . . . . . . . 164
viContents
A Source Code 167
A.1 ASCII versions of mathematical symbols . . . . . . . . . . . . 167
A.2 Definitions of used library functions . . . . . . . . . . . . . . 167
A.3 Abstract heap data type . . . . . . . . . . . . . . . . . . . . . 169
A.4 Implementation of BlackCheck . . . . . . . . . . . . . . . . . 171
A.4.1 Input generators . . . . . . . . . . . . . . . . . . . . . 171
A.4.2 Testable types . . . . . . . . . . . . . . . . . . . . . . 173
A.4.3 Property combinators . . . . . . . . . . . . . . . . . . 173
A.4.4 Test annotations . . . . . . . . . . . . . . . . . . . . . 174
A.4.5 Testing with different strategies . . . . . . . . . . . . . 174
A.4.6 Auxiliary definitions . . . . . . . . . . . . . . . . . . 176
A.5 Implementation of GlassCheck . . . . . . . . . . . . . . . . . 179
A.5.1 Parallel answers . . . . . . . . . . . . . . . . . . . . . 182
A.5.2 Search strategies . . . . . . . . . . . . . . . . . . . . 184
A.5.3 Tree search . . . . . . . . . . . . . . . . . . . . . . . 185
A.6 Implementation of explicit sharing . . . . . . . . . . . . . . . 186
A.7 Benchmarks for explicit sharing . . . . . . . . . . . . . . . . 188
A.7.1 Permutation sort . . . . . . . . . . . . . . . . . . . . 188
A.7.2 Naive reverse . . . . . . . . . . . . . . . . . . . . . . 189
A.7.3 Functional logic last . . . . . . . . . . . . . . . . . . . 190
A.7.4 Nondeterministic lists . . . . . . . . . . . . . . . . . . 191
B Proofs 192
B.1 Functor laws for(a!) instance . . . . . . . . . . . . . . . . 192
B.2 Monad laws for Tree instance . . . . . . . . . . . . . . . . . . 193
B.3 Laws for CPS type . . . . . . . . . . . . . . . . . . . . . . . . 196
B.3.1 Monad laws . . . . . . . . . . . . . . . . . . . . . . . 196
B.3.2 MonadPlus laws . . . . . . . . . . . . . . . . . . . . . 197
viiList of Figures
2.1 Safe placement of 8 queens on an 88 chessboard . . . . . 28
2.2 Safe of 15 queens on an 1515 chessboard . . . 33
3.1 Search space for an arbitrary value of type[Bool] . . . . . . . 40
3.2 Level diagonalisation of[Bool] values . . . . . . . . . . . . . 50
3.3 Combined randomised level diagonalisation of[Bool] values . 51
4.1 Computation of data flow for reverse[x, y] . . . . . . . . . . . 90
4.2 Syntax of core Curry programs . . . . . . . . . . . . . . . . . 97
5.1 The laws of a monad with nondeterminism and sharing . . . 135
5.2 The laws of observing a monad with nondeterminism and
sharing in another monad with nondeterminism . . . . . . . 137
viiiList of Tables
3.1 Comparison of different strategies for black-box testing . . . . 56
3.2 Comparison of black-box and glass-box testing . . . . . . . . 71
4.1 Data flow in applications of reverse. . . . . . . . . . . . . . . 86
4.2 Experimental results of coverage-based testing . . . . . . . . . 106
4.3 Sizes of reduced sets of tests for different coverage criteria . . 107
5.1 Performance of different monadic search strategies . . . . . . 124
ixList of Tables
x