** Next:** Applications
** Up:** An Overview of MSR():
** Previous:** A Symbolic Verification Procedure

#

Implementation in CLP

Most CLP systems can be naturally used as implementation platform
for the verification methodology discussed in this paper.
CLP systems like the clp(Q,R) library of Sicstus Prolog provides
both symbolic data structures to represent multiset-based
specification languages and encapsulation operators for handling constraints at the
object level.
These features allowed us to implement a prototype in which
MSR() specifications are represented via unit clauses
that combine terms with variables and constraints like:

Here a multiset is represented as a list of atomic formulas
like and a constraints is represented (following the clp(Q,R) syntax)
as a list of linear arithmetic atomic constraints like
.
In this setting the symbolic predecessor and the entailment
operator can be naturally implemented by using *unification* (to handle
multiset matching) and querying the *constraint solver*
(for checking satisfiability, for projection, and for entailment).
This way, we must be able to transform constraints from uninterpreted terms
to active objects. Furthermore, we must be able to retrieve the results produced
by the constraint solver (that can be viewed as an oracle that puts its output on the constraint
store).
The clp(Q,R) library provides special built-in predicates for this sort of computations.
Specifically, it provides a predicate that given a constraint in input
return its simplified form (if satisfiable). Furthermore, it provides predicates that can
be used to define (in the similar input output fashion) projection over individual variables.

Using these features we have defined a library for handling (sets of) *constrained
configurations* and we have incorporate it within a least fixpoint engine with entailment
as termination test.
The prototype has been used in several applications as discussed in the following section.

** Next:** Applications
** Up:** An Overview of MSR():
** Previous:** A Symbolic Verification Procedure
Giorgio Delzanno
2003-02-03