La lecture en ligne est gratuite
Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres

Partagez cette publication

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

Un pour Un
Permettre à tous d'accéder à la lecture
Pour chaque accès à la bibliothèque, YouScribe donne un accès à une personne dans le besoin