CLP-Translated Program

Definition and Overview

A CLP-translated program is the result of translating an imperative program (e.g., a Java program) into an equivalent Constraint Logic Programming (CLP) program. The translation preserves the control flow of the original program, converts iteration into recursion, and represents each method as a set of CLP rules. Each Java method corresponds to a set of predicates in the CLP program; for example, in the motivating example the Java method lcm is translated into the predicates lcm, cont, check, and div.

The translation supports full sequential Java, including dynamic memory handling via built-in predicates and constraints acting as execution guards on each rule. Heap arguments are included in the translation, though they are sometimes omitted for readability when they do not affect the computation.

Structure of a Translated Rule

Each rule in the CLP-translated program has the form:

m(Args_in, Args_out, H_in, H_out, E, T) :- guard, b1, …, bn.

where:

m is the predicate name corresponding to the source method;
Args_in / Args_out are the input and output data arguments;
H_in / H_out are the input and output heap arguments;
E is an exception/execution-flow term used to thread control (e.g., ok, exc);
T is the trace term for m, of the form m(k, ⟨Tc_m^i, …, Tc_m^c⟩), where k is the index of the rule and Tc_m^i, …, Tc_m^c are free logic variables representing the trace terms associated with the calls to other predicates in the body b1, …, bn;
guard is a sequence of constraints that act as execution guards on the rule;
b1, …, bn is a sequence of instructions, including arithmetic operations, calls to other predicates, and built-in operations to handle the heap.

The trace term T is not a cardinal element of the translated program but is a supplementary argument with a central role for downstream analysis (symbolic execution, trace-abstraction, and trace-guided test case generation).

Symbolic Execution over CLP-Translated Programs

CLP-translated programs are symbolically executed using the standard CLP execution mechanism, with special support for the use of dynamic memory (via additional built-in predicates).

Formally, let M be a method and m its corresponding predicate in the CLP-translated program P, and let P′ be the union of P and the built-in predicates to handle dynamic memory. The symbolic execution of m is the CLP derivation tree, denoted Tm, with root m(I, O, Hi, Ho, E, T) and initial constraint store θ = {} obtained using P′.

Test Case Generation (TCG)

The symbolic execution tree of programs containing loops or recursion is in general infinite, so a termination criterion C is imposed to make the tree finite:

TmC is the finite (and possibly incomplete) symbolic execution tree of m with root m(I, O, Hi, Ho, E, T) w.r.t. C. Let B be the set of successful (terminating) branches.
A test case for m w.r.t. C is a tuple ⟨θ, T⟩, where θ is the constraint store and T is the trace term associated with a branch b ∈ B.
TCG is the process of generating the set of test cases associated with all branches in B.

Each test case produced by TCG represents a class of inputs that follow the same execution path, and its trace is the sequence of rules applied along that path. Concrete values can be produced later from the constraint stores (e.g., via labeling mechanisms in standard clpfd domains), yielding executable test cases.

Coverage Criteria in the Translated Setting

A coverage criterion is defined as a pair ⟨TC, SC⟩:

TC is a termination criterion ensuring finiteness of symbolic execution. This paper adopts loop-k, which limits to a threshold k the number of allowed loop iterations and/or recursive calls of each concrete loop or recursive method.
SC is a selection criterion that steers TCG to decide which paths of the symbolic execution tree are explored and which test cases TCG must produce.

Two structural coverage criteria are considered:

all-local-paths: requires that all local execution paths within the method under test are exercised up to a loop-k limit. This is of interest for unit testing where each method is tested in isolation.
program-points(P): given a set of program points P, requires that all of them are exercised by at least one test case up to a loop-k limit. This is appropriate for bug-detection and reachability verification; a particular case is statement coverage (up to a limit).

Trace-Abstraction (a Derived View)

The trace-abstraction of a CLP-translated program P with traces is obtained by, for every rule of P:

removing all atoms in the body of the rule except those corresponding to rule calls, and
removing all arguments from the head and from the surviving atoms of (1) except the last one (i.e., the trace term).

The trace-abstraction essentially corresponds to the control-flow graph of the program and serves as the basis for defining trace generators for structural coverage criteria. Its sliced variants (e.g., for the all-local-paths criterion) act as effective trace generators by combining the trace-abstraction with the termination criterion.

Role in Guided Test Case Generation

The trace terms of CLP-translated programs are used as input arguments to drive symbolic execution along specific paths. By supplying fully or partially instantiated traces (the latter containing free logic variables), test case generation can be guided—completely or partially—towards the paths needed to satisfy a selection criterion. This guided TCG scheme is the foundation on which trace-abstraction-based trace generators are applied.

Example (lcm / gcd / abs)

For a Java program with methods lcm (least common multiple), gcd (greatest common divisor), and abs, the equivalent CLP-translated program contains predicates such as:

lcm([A,B],[R], , ,E,lcm(1,[T])) :- A #>= B, cont([A,B],[R], , ,E,T).
lcm([A,B],[R], , ,E,lcm(2,[T])) :- A #<= B, cont([B,A],[R], , ,E,T).
cont([A,B],[R], , ,E,cont(1,[T,V])) :- gcd([A,B],[G], , ,E,T), check([A,B,G],[R], , ,E,V).
...

with the exception-flow term E and trace terms threading rule indices and sub-call traces through each predicate.