Analysis and Visualization Tools for Constraint Programming : Constraint Debugging

by Deransart, Pierre; Hermenegildo, Manuel V.; Maluszynski, Jan; Mauszynski, J.

• ISBN13: 9783540411376
• ISBN10: 3540411372
• Format: Paperback
• Copyright: 2000-10-01
• Publisher: Springer Verlag

Summary

This book is the first one entirely devoted to the topic of constraint debugging; it presents new approaches to debugging for the computational paradigm of constraint programming. The book is based on the European research project DiSCiPl. It consists of an introduction and three parts, each of them composed of several chapters. The introduction presents the DiSCiPl debugging methodology and explains how the technical chapters are related. The three parts on correctness debugging, performance debugging, and user cases offer a total of 13 consistenly written chapters.

Table of Contents

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