Debugging Systems
for Constraint Programming
Context and Motivations
Conventional programming techniques are not well suited for solving many
highly combinatorial industrial problems, like scheduling, decision making,
resource allocation or planning. Constraint Programming (CP), an emerging
software technology, offers an original approach allowing for efficient
and exible solving of complex problems, through combined implementation
of various constraint solvers and expert heuristics. Its applications are
increasingly elded in various industries.
One of the main features of CP is a new approach to software production:
the same program is progressively improved at each step of the development
cycle, from the first prototype until the final product. This makes debugging
the cornerstone of CP technology.
Topic
We consider debugging in a broad sense: it concerns both validation aspects
(to build a correct application) as well as methodological aspects (to find
the best solution to a problem by better understanding of constraint solver
behaviour). To satisfy these objectives, tools must locate and explain bugs,
and graphic tools must help interpreting program behaviour and results.
Existing tools reveal to be ineffective in most industrial situations and
tools developed for imperative or functional programming are not adapted
to the context of CP. The main reasons are that the huge numbers of variables
and constraints makes the computation state difficult to understand, and
that the non deterministic execution increases drastically the number of
computation states which must be analysed.
Objectives and Results
The goal of the proposed project is to define, to implement and to assess
novel and effective debugging systems for Constraint Programming.
The expected results of the project include:
They will allow industrialists to apply this technology readily to applications
that can be even more complex in domains such as scheduling, planning, design
or configuration.
Approach
We propose to extend three paradigms currently used in advanced debugging:
Impact of Results
The industrial end-user partners stand to benet immediately from the
proposed work, in the form of reduced cost for even more complex applications,
developed for industries in Europe.
In general, any industry using CP can benet from the proposed work.
The academic partners will use the debugging tools for education and research.
Education plays a key role for further proliferation of CP technology in
European industry. An important fallout of the
project is the possible use of such debugging systems in other declarative
languages.
Mechanisms for Take-up of the Results
The industrial vendor partners will be present throughout the project
to allow the academic results to be taken-up in the form of commercial products
and training.
Mechanisms for take-up will be:
2.1 Context and Approach
The two crucial aspects of debugging of CP applications are methodology and validation.
Within application modelling, methodological issues include the choice of a model and of a constraint system, the choice of a resolution strategy and its optimisation.
Validation is the verification of the correspondance between the program and the programmer's intention. It can be modeled by the notions of partial correctness and completeness. The main problem is to locate bugs when symptoms of incorrectness or incompleteness have been observed.
Existing debugging tools are mostly based on displaying variables and constraints, classical dynamic trace box model or GANTT chart display. Graphical tools play an important role to help the user to figure out aspects of the solutions or of an execution state. They are usually programmer oriented and are well adapted to locate simple bugs as long as not too many constraints are involved.
Present methods suffer strong limitations which make them ineffective in most industrial situations. There are two main reasons for that: the huge amount of variables and constraints makes the computation state too complex to understand, and the non determinism of the execution increases drastically the number of computation states which must be analysed.
Since CP is a declarative paradigm, it is particularly well suited to apply declarative analysis methods such as assertion based methods used in validation, and declarative debugging techniques used to locate bugs. A lot of advantages can be derived from using these methods enhanced with adapted graphic tools.
The approach of the proposed debugging systems is to combine the use of graphic tools and declarative analysis methods to assist the user and to simplify bug location.
Such debugging systems will also contribute to resolve the methodological issues, by allowing the user to understand and compare different execution strategies.
The proposed approach is based on the following paradigms:
2.2 Declarative Debugging for Declarative languages
The proposed approach for bug localisation builds up on the notion of Declarative Debugging (DD), developed first for pure logic programs and more recently adapted for other kinds of programming languages, e.g. for a subset of Pascal, and for lazy functional languages including Haskell.
Declarative debugging is based on the fact that in a declarative language (i.e. a language with a semantics which is independent of its execution model) the notion of error is declarative, i.e. a small piece of code can be identified as erroneous without referring to any operational semantics. In the case of definite programs, for example, an error will be an incorrect or, roughly speaking, a missing clause. A user observes an error symptom only by looking at results of his/her program. The basic idea of declarative debugging is that, when some symptom has been identified, the related errors may be located through a user-dialog where questions have to be answered by the user in a way which is independent of the implemented execution model. The dialog may be automatically directed in such a way that only relevant questions are asked, thus avoiding the use of long and ineffective traces.
The kind of symptom to be considered in the project are symptoms which are wrong and missing solutions. Declarative debugging can be viewed as abstract tracing. Each step requires the display of a relevant part of a complex computation state. This brings a number of research problems to be addressed in the project.
A substantial know-how has been already accumulated showing advantages and limits of declarative debugging for various programming languages. Declarative debugging appears to be very promising, but its success is related to the declarativity level of the host language.
Recent industrial practice shows that CP is effectively used in a declarative
way. There are several reasons for this. First, the added expressivity of
CP languages with regards to classical Logic Programming, and in particular
the availability of disequations and of global constraints, make the use
of cuts and negation by failure much less mandatory for programmers. Second,
CP applications are usually geared towards the exploitation of the numerical
capabilities of the language, which means that the meta-programming facilities
of the language are less used. Hence, constraint programming languages are
much more suited to the application of declarative debugging and should
benefit to a large extent from this approach.
Previous studies have shown that declarative diagnosis can be simply adapted
to the classical CLP framework, using proof tree and skeleton
notions. Nevertheless, both theoretical and practical aspects of CP forbid
direct application of this approach. Here are some of the problems which
must be further explored :
A declarative semantics which considers an incomplete constraint solver
cannot be based on the domain
or the theory
of the underlying
interpretation of constraints.
For example, let
be the constraint domain and
be the program ![]()
then
is a
-logical consequence of
but there is not a more general
computed answer. A sufficient condition for this single covering property
is the Independence of Negated Constraints (INC), but this condition is
verified by very few interesting constraint domains.
As a matter of fact, each declarative answer is covered by a set of computed
answers. Sometimes, this set is not finite: for example, let
be the constraint
domain and
be the program
. true is a
declarative answer, but is not covered by a subset of
.
Assume the relation
(resp.
) of the previous
examples specifies that x is an integer (resp. a real number). From
a declarative viewpoint, we cannot consider that the lack of an answer more
general than true is a symptom of an error in the program. If the
program is correct then its declarative semantics must verify intended properties
of the programmer.
Moreover, in addition to the answer constraint which can be a complex constraint with many existentially quantified variables, the system displays value domain approximations of the goal variables (this is sometimes the single information considered by the user). We have also to take into account these approximations to elaborate user-adapted diagnosers.
The above problems show that new theoretical foundations are necessary to build effective debugging systems for industrial applications of Constraint Programming.
The semantics based on a rejection criterion presented in abstracts the
interpretation of constraint satisfaction. The rejection criterion can be
deduced from a constraint domain
, a constraint theory
(not necessarily satisfaction complete) or an algorithm of constraint
satisfaction (not necessarily complete). We believe that incorrectness declarative
diagnosis can be studied in this framework, considering the incompleteness
of solvers. However, the rejection criterion must be extended to study insufficiency
problems.
Declarative diagnosis algorithms of logic programs use well-known properties
of logic programs (for example, for insufficiency, the single covering properties).
Therefore, there is the need to find new definitions of wrong and missing
answers adapted to the more general framework of constraint programming.
Then, there is the need to find new declarative diagnosis algorithms in
this context.
2.3 Assertion based methods
Declarative debugging is based on the assumption that the user is able to indicate which of the intermediate answers are erroneous. In the case of CP the intermediate answers are constraints representing sets of solutions. In the case of very complex formulae, the user may not be able to decide whether all the solutions of such a constraint correspond to his/her expectations. Thus, querying the user directly about complex constraints in the debugging process should be avoided. Therefore we focus our attention on the possible ways of overcoming the difficulty by adding assertions to the language.
Assertions are partial specifications which are provided by the programmer. They can be attached to the program's predicates, constraints or variables, and they represent expected properties of the program. Assertions are associated to a notion of correctness. A program is correct w.r.t. given assertions if the assertions are satisfied in some formally defined sense.
Two kinds of assertions have been considered. The assertions of the first kind describe properties of the expected answers of the program, thus properties of the expected model. They are often called declarative properties of the program, since they do not depend on the operational semantics (provided that this semantics is sound). A program is correct w.r.t. an assertion if the assertion is entailed by every answer computed by the program. The proof method proposed by Clark is a classical approach to proving declarative properties. A modular approach to proving declarative properties, known as the annotation method has been developed by Deransart. Clark's method can be seen as a special case of the annotation method. In both methods some verification conditions are to be checked locally for each clause. In the context of program debugging this means that the clauses which satisfy the local verification conditions for expected declarative properties may be excluded from debugging, while the other ones may need correction.
Another kind of assertions, concerning execution of the program with Prolog computation rule has been discussed by Drabent and Maluszynski. Such assertions describe input-output behaviour of the predicates. More precisely, they describe the form of predicate calls during the execution of the program, and also the form of the answers for the calls satisfying the assertions. Therefore the described properties are sometimes called dynamic or run-time properties. A program is correct if the initial call satisfying the input assertion of its predicate will result in a computation where every call of a predicate satisfies the input assertion, and every intermediate answer satisfies the output assertion. The proof method of Drabent and Maluszynski defines verification conditions which have to be checked locally for each clause to guarantee correctness of the program. It is worth noticing that the run-time assertions are potentially very useful in the context of debugging. Due to the locality of verification conditions, every clause proved to be correct need not be taken into consideration in debugging of the program. For the remaining clauses a run-time test may be installed for checking whether the form of the local call conforms to the user's expectation stated as the assertion. However, the verification conditions of Drabent and Maluszynski refer to the constraint solving mechanism (in particular to the unification mechanism in the case of Prolog) and are therefore rather difficult to check in practice.
A special kind of run-time assertions where the verification conditions become more simple is known under the name of directional types..
The recent work of Boye and Maluszynski shows a refinement of the verification conditions for directional types and relates the type checking techniques to the annotation method of Deransart.
The work of E. Vétillard shows that directional types are applicable for debugging of CP programs. The assertions are here considered as constraints on an extended constraint structure, and their proof is performed using abstract interpretation techniques. The use of such approximated techniques simplifies the proof, and some experimental results done on a subset of Prolog III have shown that this did not incur a significant precision loss in the proof.
We plan to further investigate the role of abstract interpretation not only in testing assertions, but also in generating them. In particular, assertions can generally be viewed as stating properties at the predicate level in some abstract domain that is understandable to the user. As mentioned before, abstract interpretation techniques can be applied to check such user supplied assertions. Additionally, since the main role of global program analysis based on abstract interpretation is to derive properties of the program, the technique can also be applied to derive new assertions. Such new assertions can for example state properties at intermediate points within the program, providing new, more detailed information for the user. Furthermore, it is also possible to accurately generate missing predicate level assertions from others present in the program. This can greatly reduce the work for the programmer in that when so desired it makes it possible to state assertions only for critical predicates. Also, it is usually the case that small changes to programs take place during program development and debugging. In such a context, assertion information can be updated efficiently and automatically by means of incremental abstract interpretation techniques. We plan to use incremental analysis techniques which are capable of dealing with both user-supplied assertions and those automatically generated. We also plan to extend the techniques to deal with commercially available languages.
In addition to the existence of such static proof mechanisms, which make it possible to debug constraint programs at compile-time, the assertions can be used in the framework of declarative debugging. By providing additional information about the program, the assertions can help the declarative debugging process by answering automatically to some queries. Furthermore, the availability of local static proof methods makes it possible to exclude some clauses altogether from the declarative debugging querying. All this results in a simplification of the dialog between the machine and the programmer during a declarative debugging session.
The dialog itself can be instrumented through the use of assertions, i.e., allowing the user to introduce assertions during a debugging dialog. In such a dynamic use of assertions, there are two important and related points to consider. First, how such assertions can affect, and can be used to incrementally modify, the previous assertions already checked to be correct, so that the annotated program remains correct w.r.t. the old and new assertions. Second, how
to treat programs annotated with assertions. Additionally, these issues should also be considered for constraint languages with complex computation rules, such as passive constraints, delay primitives, and/or suspension of computations. Finally, we plan to investigate other methods such as non-failure analysis and determinacy analysis which can also aid in the program development task.
2.4. Graphics based tools
In the declarative debugging process, one of the research problems mentioned above is to display complex computation states referenced during the dialog. A query to the user comes in the form of a complex constraint, which may sometimes be difficult for the user to understand, and thus to answer. We propose to develop visualization tools in order to help the user to understand such complex constraints, as well as for other purposes related to (performance) debugging, such as visualizing complex search spaces.
There are many challenges involved in developing useful visualization tools for the above mentioned applications. The theory of CLP provides a uniform view of the CLP computation process. There is a generic framework followed by all CP systems, but each system then implements specific types of constraints. Based on the general CP scheme it is possible to develop generic constraint visualization tools, which can be used for any constraint domain, including user--defined constraints. However, for some well--known constraint domains, the user expects some specific properties to hold, which the visualizer should take into account in order to provide a more intuitive depiction of the computation process. This can be accomplished by instantiating the general visualization paradigm with the actual characteristics of the constraint system being used. This instantiation is, in many cases, non trivial (for example, in the cases where different constraint domains are being used at the same time), and can lead to visualization paradigms which look completely different from the generic one, but with which the same underlying theoretical background is shared.
The actual form in which the dialog between the user and the debugging
system is maintained is, in principle, an orthogonal issue. Possible interfaces
between the user and the system are geometrical representations of the computation
space represented by a particular (set of) constraint(s), projections of
constraints on a set of variables, representation of the current subset
of the search space by means of intervals associated with variables, etc.
Adapting them to different constraint systems, as suggested in the above
paragraph, can in principle be performed for any of the visualization systems
chosen. For example, generic intervals for each variable can be represented
as intervals in
for clp(
), as sets of discrete
points in clp (fd) or as subsets of the Herbrand universe in clp(
). Designing intuitive constraint representations is a task in which
work remains to be done, and which will be addressed in this project.
As mentioned before, one additional important characteristic of the visualization systems to be used in debugging is that they should make it easier for the user to understand the questions produced by the debugger, by making reference to easily recognizable entities such as, for example, original query variables. This can be accomplished by using two different approaches:
Such techniques can be implemented with the use of sophisticated graphic tools. The XGIP module developed by COSYTEC allows the user to design and develop sophisticated graphical interfaces. It is desirable to build drag-and-drop tools on top of XGIP to allow the user to define the displays with the right level of abstraction.
Graphic tools may also be used to update computation states. For example, with the Gantt Chart, the user may post additional constraints via the graphic interface, even to the point of instantiating variables. This interaction can be used within declarative debugging, when the user is queried about more specific states.
A desirable characteristic in the visualization systems to be developed is the ability of performing an abstraction of the represented constraints. This means being able to provide the user with views at different levels of detail, which allow easily understanding the ``big picture'' as well as the more concrete details. This abstraction process can take several forms, depending on the conceptual dimension which is being abstracted: it might very well be as simple as zooming in and out (as done, for example, where a complex process structure is visualized via abstracting sequential tasks and using zooming to move between levels of concretization, and color coding to represent physical resources), or as complex as allowing the user to fade away some classes of constraints (i.e., the user might be interested only on visualizing constraints where variables have a semi--infinite range, or only in constraints which have been suspended due to the inability of the solver to treat them directly). Several interesting dimensions (which in some cases depend on the particular solver being used) must be identified, and the visualization paradigm for them devised.
From a practical point of view, all the tools which implement these visualization ideas and designs need to be easily plugged into existing CP systems. This leads to the need of providing a generic interface with which the constraint language and debugging system can maintain a two--way communication with the visualization. A generic toolkit should be devised to this end. This toolkit can be designed to take into account special characteristics of particular CP systems in much the same way as the generic visualization paradigm can be.
An interesting issue, subject to further study, is representing not only the constraint store as a set of (dis)equations in a (or several) given domain(s), but reflecting how the current state of the constraint store affects the execution flow of the programs. An approach along those lines was the one taken for Prolog. The CP paradigm offers a much richer setting: the set of active and passive constraints associated with every point in the program can be visualized, and the debugger would tell the user why a given execution path was chosen. Special attention should be given to disjunctive constraints which can be seen as encoding alternative execution paths, thus allowing the programs to delay speculative computations and to achieve better performance.
2.5 Research Topics
In addition to the development work (some details are provided in the description of the tasks below), this approach leads to three families of research problems, which have been identified and must be investigated in order to reach the objectives of the project. They are summarized below:
Our approach in handling assertions is to consider different kinds of language extensions including assertions, possibly defined in different languages, either inside the constraints, or outside, as comments. The research will thus include the following points.
Complex constraints may be displayed using graphics and therefore, new forms of interaction during debugging must be designed. Moreover, the display of the history of variables and constraints, showing past events and deductions, will help the user to understand the behavior of the program.
As further explained in Chapter 6 on the proposers, the consortium is confident that all required expertise is available within the consortium. Some risk does exist, linked to the research topics described above, but the risk level is acceptable.