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(${\mathscr C}$) specifications are represented via unit clauses that combine terms with variables and constraints like:

$$r([p(X),q(Y)],[r(Z),t(W)],\{X>Y,Z=Y,W=Y+1\}).$$

Here a multiset is represented as a list of atomic formulas like $[p(X),q(Y)]$ and a constraints is represented (following the clp(Q,R) syntax) as a list of linear arithmetic atomic constraints like $\{X>Y,Z=Y,W=Y+1\}$. 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.