The transformation of constraint logic programs (CLP programs)has been shown to be an effective methodologyfor verifying properties of imperative programs.By following this methodology, we encode the negationof a partial correctness property of an imperativeprogram prog as a predicate incorrect defined by a CLP program P, and we show thatprog is correct by transforming P intothe empty program through the applicationof semantics preserving transformation rules.Some of these rules perform replacements of constraintsthat encode properties of the data structures manipulatedby the program prog.In this paper we show that Constraint Handling Rules (CHR)are a suitable formalism for representing and applyingconstraint replacements during the transformation of CLP programs.In particular, we consider programs that manipulate integerarrays and we present a CHR encoding of a constraint replacementstrategy based on the theory of arrays.We also propose a novel generalization strategy forconstraints on integer arrays that combinesthe CHR constraint replacement strategywith various generalization operator for linear constraints,such as widening and convex hull.Generalization is controlled by additional constraintsthat relate the variable identifiers in the imperativeprogram and the CLP representation of their values.The method presented in this paper has been implemented andwe have demonstrated itseffectiveness on a set ofbenchmark programs taken from the literature.
A Folding Algorithm for Eliminating Existential Variables from Constraint Logic Programs
