| Introduction | p. 1 |
| Correctness Debugging | |
| An Assertion Language for Constraint Logic Programs | p. 23 |
| Introduction | p. 23 |
| Assertions in Program Validation and Debugging | p. 27 |
| Assertion Schemas for Execution States | p. 29 |
| An Assertion Schema for Success States | p. 30 |
| Adding Preconditions to the Success Schema | p. 31 |
| An Assertion Schema for Call States | p. 32 |
| An Assertion Schema for Query States | p. 33 |
| Program-Point Assertions | p. 34 |
| Logic Formulae about Execution States | p. 35 |
| An Assertion Schema for Declarative Semantics | p. 37 |
| Assertion Schemas for Program Completeness | p. 38 |
| Status of Assertions | p. 40 |
| An Assertion Schema for Computations | p. 44 |
| Logic Formulae about Computations | p. 45 |
| Defining Property Predicates | p. 46 |
| Declaring Property Predicates | p. 47 |
| Defining Property Predicates for Execution States | p. 48 |
| Defining Property Predicates for Computations | p. 50 |
| Approximating Property Predicates | p. 51 |
| Syntax of and Extensions to the Assertion Language | p. 52 |
| Syntax of the Assertion Language | p. 53 |
| Grouping Assertions: Compound Assertions | p. 54 |
| Some Additional Syntactic Sugar | p. 56 |
| Discussion | p. 58 |
| References | p. 59 |
| A Generic Preprocessor for Program Validation and Debugging | p. 63 |
| Introduction | p. 63 |
| Design of the Preprocessor | p. 64 |
| Chapter Outline | p. 68 |
| Architecture and Operation of the Preprocessor | p. 69 |
| The Syntax Checker | p. 69 |
| The Static Analysers | p. 72 |
| Consistency of the Analysis Results | p. 73 |
| The Assertion Normaliser | p. 74 |
| The Assertion Comparator | p. 75 |
| Assertions for System Predicates | p. 75 |
| Assertions for User-Defined Predicates | p. 77 |
| Compile-Time Checking | p. 79 |
| Run-Time Checking | p. 85 |
| Evaluating Atomic Logic Formulae | p. 86 |
| A Program Transformation for Assertion Checking 89 | |
| Customising the Preprocessor for a CLP System: The CiaoPP and CHIPRE Tools | p. 93 |
| Describing Built-Ins Using Assertions | p. 94 |
| System Dependent Code for Run-Time Checking | p. 97 |
| A Sample Debugging Session with the Ciao System | p. 98 |
| Some Practical Hints on Debugging with Assertions | p. 103 |
| References | p. 104 |
| Assertions with Constraints for CLP Debugging | p. 109 |
| Introduction | p. 109 |
| Form of Assertions | p. 110 |
| Syntax and Meaning of Assertions | p. 110 |
| The Basic Constructs | p. 111 |
| Correctness Proofs | p. 112 |
| Implementation | p. 112 |
| Example of a Verification | p. 113 |
| Incompleteness Introduced by the Solvers | p. 114 |
| Full Example | p. 115 |
| Samples of Compilations | p. 116 |
| Run-Time Checking | p. 118 |
| Conclusion | p. 119 |
| References | p. 120 |
| Locating Type Errors in Untyped CLP Programs | p. 121 |
| Introduction | p. 121 |
| The Specification Language | p. 124 |
| Calls and Successes of a CLP Program | p. 124 |
| Describing Sets of Constrained Atoms | p. 126 |
| An Example Diagnosis Session | p. 128 |
| The Diagnosis Method | p. 133 |
| Correct and Incorrect Clauses | p. 134 |
| Incorrectness Diagnosis | p. 137 |
| Delays | p. 138 |
| The Diagnosis Tool | p. 141 |
| Limitations of the Approach | p. 143 |
| Related Work | p. 146 |
| Conclusions and Future Work | p. 148 |
| References | p. 149 |
| Declarative Diagnosis in the CLP Scheme | p. 151 |
| Introduction | p. 151 |
| Basic Notions of Symptom and Error | p. 154 |
| Connection between Symptom and Error via Proof-Trees | p. 156 |
| Diagnosis Algorithm | p. 160 |
| Abstract Proof-Trees | p. 163 |
| Implementation | p. 167 |
| A Diagnosis Session | p. 170 |
| Conclusion | p. 172 |
| References | p. 173 |
| Performance Debugging | |
| Visual Tools to Debug Prolog IV Programs | p. 177 |
| Introduction | p. 177 |
| Presentation of the Execution Tree Viewer | p. 178 |
| The Box Model | p. 178 |
| Execution Trees | p. 179 |
| The Prolog IV Execution Tree Viewer | p. 183 |
| Textual Information in the Canvas | p. 184 |
| Viewer Functions Description | p. 184 |
| Colouring Boxes | p. 185 |
| Replay Mode | p. 186 |
| "Replay-Left Mode" Option | p. 186 |
| "Show all Tries" Option | p. 187 |
| Miscellaneous | p. 187 |
| Working with the Debugger | p. 187 |
| Setting a Temporary Break-Point | p. 188 |
| Replaying the Execution | p. 188 |
| About Implementation | p. 189 |
| Conclusion | p. 190 |
| References | p. 190 |
| Search-Tree Visualisation | p. 191 |
| Introduction | p. 191 |
| Related Work | p. 192 |
| Principles of Operation | p. 193 |
| Program Structure | p. 193 |
| Symptoms | p. 193 |
| Operating Mode | p. 194 |
| System Requirements | p. 195 |
| Interface | p. 195 |
| Views | p. 197 |
| Types of Views | p. 197 |
| Tree View | p. 198 |
| Variable Views | p. 201 |
| Constraint Views | p. 203 |
| Propagation View | p. 205 |
| Current State and Further Development | p. 206 |
| Conclusion | p. 207 |
| References | p. 208 |
| Towards a Language for CLP Choice-Tree Visualisation | p. 209 |
| Introduction | p. 209 |
| CLP: Syntax, Semantics and State Properties | p. 211 |
| Syntax | p. 211 |
| Constraint Domains | p. 212 |
| Constrained Predication and D-Atom | p. 212 |
| Operational Semantics | p. 213 |
| CLP Search-Tree | p. 214 |
| Labelling | p. 216 |
| State Properties | p. 217 |
| Tree Pruning and CLP Choice-Tree | p. 219 |
| Unique Minimal Pruned Tree | p. 219 |
| Minimal Pruned Tree Construction | p. 221 |
| CLP Choice-Tree | p. 223 |
| A Language to Specify Views | p. 224 |
| Node Selection | p. 225 |
| Arc Selection | p. 225 |
| Node and Arc Selection Using Differential Information | p. 226 |
| View Specification | p. 227 |
| Implementation and Examples | p. 227 |
| Displaying the Full Concrete Choice-Tree | p. 228 |
| A General Criterion for a More Synthetic View | p. 229 |
| View of the Labelling | p. 230 |
| Use of State Properties | p. 232 |
| Comparison of Labelling Strategies | p. 232 |
| Conclusion | p. 234 |
| References | p. 236 |
| Tools for Search-Tree Visualisation: The APT Tool | p. 237 |
| Introduction | p. 237 |
| Visualising Control | p. 238 |
| The Programmed Search as a Search Tree | p. 239 |
| Representing the Enumeration Process | p. 240 |
| Coupling Control Visualisation with Assertions | p. 241 |
| The APT Tool | p. 242 |
| Event-Based and Time-Based Depiction of Control | p. 245 |
| Abstracting Control | p. 248 |
| Conclusions | p. 250 |
| References | p. 251 |
| Tools for Constraint Visualisation: The VIFID/TRIFID Tool | p. 253 |
| Introduction | p. 253 |
| Displaying Variables | p. 254 |
| Depicting Finite Domain Variables | p. 254 |
| Depicting Herbrand Terms | p. 258 |
| Depicting Intervals or Reals | p. 258 |
| Representing Constraints | p. 259 |
| Abstraction | p. 263 |
| Abstracting Values | p. 263 |
| Domain Compaction and New Dimensions | p. 264 |
| Abstracting Constraints | p. 268 |
| Conclusions | p. 270 |
| References | p. 270 |
| Debugging Constraint Programs by Store Inspection | p. 273 |
| Introduction | p. 273 |
| Constraint Logic Programming in a Nutshell | p. 274 |
| Arising Difficulties when Debugging Constraint Programs | p. 276 |
| Constraint Programming Efficiency | p. 276 |
| Drawbacks of CP Expressiveness | p. 278 |
| Visualising the Store | p. 278 |
| Structuring the Store | p. 279 |
| S-Boxes | p. 281 |
| Presentation of the Debugger Prototype | p. 285 |
| Implementation of the S-Box Based Debugger | p. 287 |
| Modification of the Backtracking Process | p. 291 |
| Modification of the Propagation Process | p. 291 |
| Handling the S-Boxes | p. 293 |
| Conclusion | p. 294 |
| References | p. 296 |
| Complex Constraint Abstraction: Global Constraint Visualisation | p. 299 |
| Introduction | p. 299 |
| Global Constraint Concepts | p. 301 |
| Cumulative | p. 301 |
| Diffn | p. 302 |
| Cycle | p. 302 |
| Among | p. 303 |
| Principles of Operation | p. 303 |
| Class Structure | p. 303 |
| Callbacks | p. 305 |
| API | p. 306 |
| Interface to Search-Tree Tool | p. 307 |
| Use Outside Search-Tree Tool | p. 308 |
| Cumulative Visualisers | p. 308 |
| Cumulative Resource | p. 308 |
| Bin Packing | p. 311 |
| Diffn Visualisers | p. 311 |
| Placement 2D | p. 311 |
| Placement Remains | p. 311 |
| Cycle Visualiser | p. 313 |
| Geographical Tour | p. 313 |
| Graph Lines | p. 314 |
| Interaction between Visualisers | p. 315 |
| Conclusions | p. 315 |
| References | p. 316 |
| Test Cases | |
| Using Constraint Visualisation Tools CHelmut Simonis | p. 321 |
| Introduction | p. 321 |
| Debugging Scenarios | p. 322 |
| Finding New Variable/Value Orderings | p. 323 |
| Comparing Two Heuristics | p. 328 |
| Adding Redundant Constraints | p. 331 |
| Discovering Structure in the Problem | p. 334 |
| Identifying Weak Propagation | p. 336 |
| Case Studies from Industry | p. 337 |
| Scheduling Application Involving Setup Cost | p. 337 |
| Tank Scheduling Application | p. 340 |
| Layout of Mechanical Objects: Graph Colouring | p. 344 |
| Layout of Mechanical Objects: Physical Layout | p. 348 |
| Analysis and Possible Improvements | p. 351 |
| Need for a Debugging Methodology | p. 351 |
| Program Improvement Due to the Use of Debugging Tools | p. 351 |
| General Conclusions on the CHIP Graphical Debugging Tools | p. 352 |
| Suggestions for Extensions to the CHIP Debugging Tools | p. 353 |
| Conclusions | p. 355 |
| References | p. 356 |
| Author Index | p. 357 |
| Subject Index | p. 359 |
| Table of Contents provided by Publisher. All Rights Reserved. |