Program transformation systems have been widely studied within thefield of logic programs. This paper extends such systems to constraintlogic programs. First, the authors define a semantics for constraintlogic programs that extends the C-semantics of logic programs, namely,the semantics given by the set of correct answer substitutions. For suchsemantics, a model-theoretic, an operational, and a fixed-pointcharacterization are given and proven to be equivalent. Then, for eachtransformation rule of the system, the correctness is proven with regardto such semantics.

The paper is an interesting extension of previous proposals[1–3] to constraint logic programs. It is clearly written, andeach choice is discussed and motivated. The proofs are interesting inthemselves, since they are all based on the fixed-point semantics andare also somehow “syntactical.” I found thechoice of C-semantics questionable, since in practical applications onewants to preserve the computed answer substitutions (given byS-semantics). The bibliography is good, but not exhaustive ontransformations, which also preserve termination properties.