This volume constitutes the thoroughly refereed post-conference proceedings of the 19th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2009, held in Coimbra, Portugal, during September 9-11, 2009. The 14 revised full papers presented together with one invited talk were carefully reviewed and selected for inclusion in the book. LOPSTR traditionally solicits papers in the areas of specification, synthesis, verification, transformation, analysis, optimization, composition, security, reuse, applications and tools, component-based software development, software architectures, agent-based software development, and program refinement.
Author(s): Danny De Schreye
Edition: 1st Edition.
Publisher: Springer
Year: 2010
Language: English
Pages: 213
Introduction......Page 9
Accuracy vs. Efficiency......Page 10
Concluding Remarks......Page 11
References......Page 12
Introduction......Page 13
Encoding CTL* Model Checking as a Logic Program......Page 14
Syntax and Semantics of -Programs......Page 15
Encoding the CTL* Satisfaction Relation as an -Program......Page 17
Transformation to Monadic -Programs......Page 19
A Proof Method for Monadic -Programs......Page 24
Related Work and Concluding Remarks......Page 26
References......Page 28
Introduction......Page 30
CHR Syntax......Page 31
The Abstract CHR Semantics......Page 32
Representing the CHR Constraint Store in Prolog......Page 33
Representing the Abstract Semantics of CHR in Prolog......Page 34
Transformation Summary......Page 35
Application of the Transformation to Type Analysis......Page 39
Evaluation of the Transformation......Page 41
Conclusion......Page 43
References......Page 44
Introduction......Page 45
Preliminaries on Logic Programming......Page 46
Dependency Triple Framework......Page 47
Dependency Graph Processor......Page 50
Reduction Pair Processor......Page 51
Modular Transformation Processor to Term Rewriting......Page 53
Experiments and Conclusion......Page 57
References......Page 59
Introduction......Page 60
Preliminaries......Page 61
Goal-Directed Dependency Pairs......Page 63
Dependency Graphs......Page 64
Usable Rules......Page 65
Relative Termination......Page 68
Termination of Narrowing via Relative Termination......Page 69
Results and Discussion......Page 72
References......Page 73
Introduction......Page 75
Preliminaries on Logic Programming (without Grouping)......Page 76
Well-Moded Logic Programs......Page 77
Grouping in Prolog......Page 78
Semantics of Atomic moded_bagof Queries......Page 80
Using moded_bagof in Queries and Programs......Page 81
Properties......Page 83
Related Work......Page 86
References......Page 88
Introduction......Page 90
A Framework for Unfold/Fold Transformation......Page 91
Transformation Rules......Page 92
Correctness of Unfold/Fold Transformation......Page 95
Coinductive Proofs via Unfold/Fold Transformations......Page 99
Conclusion......Page 103
References......Page 104
Introduction......Page 105
Preliminaries......Page 106
Coinductive SLDNF Resolution......Page 107
Illustrative Examples......Page 110
Correctness of co-SLDNF Resolution......Page 114
Applications of co-LP with co-SLDNF......Page 118
References......Page 119
Introduction......Page 121
The Bilattice FOUR of Four Truth Values......Page 124
The Four-Valued Predicate Logic......Page 125
The Lattice of Predicate Transformers......Page 126
Predicate Transformers for Basic Statements......Page 127
Logical Connectives for Partial Predicates......Page 128
Refinement of Conditional Controls......Page 129
Translating Conjunctions and Disjunctions into Explicit Controls......Page 131
Refining Exception Handling......Page 132
References......Page 134
Introduction......Page 136
Overview......Page 139
Constraint Generation......Page 140
Properties......Page 142
Search......Page 144
Generalized Data Structures......Page 145
Applications......Page 146
Related Work and Conclusion......Page 148
References......Page 149
Introduction......Page 151
BUpL Agents by Example......Page 153
Meta-controlling BUpL Agents with Rewrite Strategies......Page 155
Formalising Test Cases......Page 157
Using Rewrite Strategies to Define Test Drivers......Page 158
A Running Example......Page 163
References......Page 165
Introduction......Page 166
Problems of Classical Partial Evaluation......Page 167
Basic Setting......Page 168
Promotion: Lazy Choice Points......Page 170
Code Generation and Local Control......Page 172
Global Control......Page 173
Experimental Results......Page 174
More Related Work......Page 177
References......Page 178
Introduction......Page 181
Motivating Example: Mergesort......Page 183
Setting......Page 184
Eventual Independence......Page 185
Inferring Eventual Independence......Page 187
Synchronized Pipelining......Page 188
Extensions......Page 189
Motivating Example Revisited......Page 191
Experimental Results......Page 192
Related Work......Page 193
Conclusion......Page 194
References......Page 195
Introduction......Page 196
A Program Analysis Written as a Datalog Program......Page 198
From Datalog to Maude......Page 199
Answer Representation......Page 200
A Glimpse of the Transformation......Page 202
Formal Definition of the Transformation......Page 203
The Transformation......Page 204
Correctness of the Transformation......Page 206
Comparison w.r.t. a Previous Rewriting-Based Implementation......Page 207
Comparison w.r.t. Other State-of-the-Art Datalog Solvers......Page 208
Analyzing Java Programs with Reflection......Page 209
References......Page 211
