You are an expert at summarizing long articles. Proceed to summarize the following text: 
test data generation ( tdg ) aims at automatically generating test - cases for interesting test _ coverage criteria_. the coverage criteria measure how well the program is exercised by a test suite . examples of coverage criteria are : _ statement coverage _ which requires that each line of the code is executed ; _ path coverage _ which requires that every possible trace through a given part of the code is executed ; etc . there are a wide variety of approaches to tdg(see @xcite for a survey ) . our work focuses on _ glass - box _ testing , where test - cases are obtained from the concrete program in contrast to _ black - box _ testing , where they are deduced from a specification of the program . also , our focus is on _ static _ testing , where we assume no knowledge about the input data , in contrast to _ dynamic _ approaches  @xcite which execute the program to be tested for concrete input values . the standard approach to generating test - cases statically is to perform a _ symbolic _ execution of the program  @xcite , where the contents of variables are expressions rather than concrete values . the symbolic execution produces a system of _ constraints _ consisting of the conditions to execute the different paths . this happens , for instance , in branching instructions , like if - then - else , where we might want to generate test - cases for the two alternative branches and hence accumulate the conditions for each path as constraints . the symbolic execution approach is usually combined with the use of _ constraint solvers _ in order to : handle the constraints systems by solving the feasibility of paths and , afterwards , to instantiate the input variables . tdg for declarative languages has received comparatively less attention than for imperative languages . in general , declarative languages pose different problems to testing related to their own execution models , like laziness in functional programming ( fp ) and failing derivations in constraint logic programming ( clp ) . the majority of existing tools for fp are based on black - box testing ( see e.g.  @xcite ) . an exception is @xcite where a glass - box testing approach is proposed to generate test - cases for curry . in the case of clp , test - cases are obtained for prolog in  @xcite ; and very recently for mercury in  @xcite . basically the test - cases are obtained by first computing constraints on the input arguments that correspond to execution paths of logic programs and then solving these constraints to obtain test inputs for such paths .    in recent work @xcite , we have proposed to employ existing _ partial evaluation _ ( pe ) techniques developed for clpin order to automatically generate _ test - case generators _ for glass - box testing of bytecode . pe @xcite is an automatic program transformation technique which has been traditionally used to specialise programs w.r.t . a known part of its input data and , as futamura predicted , can also be used to compile programs in a ( source ) language to another ( object ) language ( see @xcite ) . the approach to tdgby pe of @xcite consists of two independent clp pe phases . ( 1 ) first , the bytecode is transformed into an equivalent ( decompiled ) clp program by specialising a bytecode interpreter by means of existing pe techniques . ( 2 ) a second pe is performed in order to supervise the generation of test - cases by execution of the clp decompiled program . interestingly , it is possible to employ control strategies previously defined in the context of clp pe in order to capture _ coverage criteria _ for glass - box testing of bytecode . a unique feature of this approach is that , this second pe phase allows generating not only test - cases but also test - case _ generators_. another important advantage is that , in contrast to previous work to tdgof bytecode , it does not require devising a dedicated symbolic virtual machine .    in this work , we study the application of the above approach to tdgby means of pe to the prolog language . compared to tdgof an imperative language @xcite , dealing with prolog brings in as the main difficulty to generate test - cases associated to failing computations . this happens because an intrinsic feature of pe is that it only produces results associated to the _ non - failing _ derivations . while this is what we need for tdgof an imperative language ( like bytecode above ) , we now want to capture non - failing derivations in prolog and still rely on a standard partial evaluator . our proposal is to transform the original prolog program into an equivalent prolog program with explicit failure by partially evaluating a prolog interpreter which captures failing derivations w.r.t . the input program . this transformation is done in the phase ( 1 ) above . as another difference , in the case of bytecode , the underlying constraint domain only manipulates integers . however , the above phase ( 2 ) should properly handle the data manipulated by the program in the case of prolog . compared to existing approaches to tdgof prolog  @xcite , our approach basically is of interest for bringing the advantages which are inherent in tdgby pe to the field of prolog :    * it is _ more powerful _ in that we can produce test - case generators which are clp programs whose execution in clp returns further test - cases on demand without the need to start the tdg process from scratch ; * it is more _ flexible _ , as different coverage criteria can be easily incorporated to our framework just by adding the appropriate local control to the partial evaluator . * it is _ simpler _ to implement compared to the development of a dedicated test - case generator , as long as a clp partial evaluator is available . the rest of the paper is organized as follows . in the next section , we give some basics on pe of logic programs and describe in detail the approach to tdgby pe proposed in @xcite . [ sec : control_flow ] discusses some fundamental issues like the prolog control - flow and the notion of computation path . then , sect . [ sec : explicit_failure ] describes the program transformation to make failure explicit , sect . [ sec : gener - test - cases ] outlines existing methods to properly handle symbolic data during the tdg phase , and finally sect . [ sec : future ] concludes and discusses some ideas for future work . in this section we recall the basics of partial evaluation of logic programming and summarize the general approach of relying on partial evaluation of clp for tdg of an imperative language , as proposed in @xcite . we assume familiarity with basic notions of logic programming and partial evaluation ( see e.g.  @xcite ) . partial evaluation is a semantics - based program transformation technique which specialises a program w.r.t . given input data , hence , it is often called _ program specialisation_. essentially , partial evaluators are non - standard interpreters which evaluate goals as long as termination is guaranteed and specialisation is considered profitable . in logic programming , the underlying technique is to construct ( possibly ) _ incomplete _ sld trees for the set of atoms to be specialised . in an incomplete tree , it is possible to choose _ not _ to further unfold a goal . therefore , the tree may contain three kinds of leaves : failure nodes , success nodes ( which contain the empty goal ) , and non - empty goals which are not further unfolded . the latter are required in order to guarantee termination of the partial evaluation process , since the sld being built may be infinite . even if the sld trees for fully instantiated initial atoms ( as regards the _ input _ arguments ) are finite , the sld trees produced for partially instantiated initial atoms may be infinite . this is because the sld for partially instantiated atoms can have ( infinitely many ) more branches than the actual sld tree at run - time . the role of the _ local control _ is to determine how to construct the ( incomplete ) sld trees . in particular , the _ unfolding rule _ decides , for each resolvent , whether to stop unfolding or to continue unfolding it and , if so , which atom to select from the resolvent . on the other hand , partial evaluators need to compute sld - trees for a number of atoms in order to ensure that all atoms which appear in non - failing leaves of incomplete sld trees are `` covered '' by the root of some tree ( this is known as the closedness condition of partial evaluation @xcite ) . the role of the _ global control _ is to ensure that we do not try to compute sld trees for an infinite number of atoms . the usual way of achieving this is by applying an _ abstraction operator _ which performs `` generalizations '' on the atoms for which sld trees are to be built . the global control returns a set of atoms @xmath0 . finally , the partial evaluation can then be systematically extracted from the set @xmath0 ( see @xcite for details ) . traditionally , there have been two different approaches regarding the way in which control decisions are taken , _ on - line _ and _ off - line _ approaches . in _ online _ pe , all control decisions are dynamically taken during the specialisation phase . in _ offline _ pe , a set of previously computed annotations ( often manually provided ) gives information to the control operators to decide , 1 ) when to stop unfolding ( _ memoise _ ) in the local control , and 2 ) how to perform generalizations in the global control . the development of pe techniques has allowed the so - called `` interpretative approach '' to compilation which consists in specialising an interpreter w.r.t .  a fixed object code . interpretive compilation was proposed in futamura s seminal work @xcite , whereby compilation of a program @xmath1 written in a ( _ source _ ) programming language @xmath2 into another ( _ object _ ) programming language @xmath3 is achieved by partially evaluating an interpreter for @xmath2 written in @xmath3 w.r.t . the advantages of interpretive ( de-)compilation w.r.t.dedicated ( de-)compilers are well - known and discussed in the pe literature ( see , e.g. , @xcite ) . very briefly , they include : _ flexibility _ , it is easier to modify the interpreter in order to tune the decompilation ( e.g. , observe new properties of interest ) ; _ easier to trust _ , it is more difficult to prove that ad - hoc decompilers preserve the program semantics ; _ easier to maintain _ , new changes in the language semantics can be easily reflected in the interpreter .      in recent work , we have proposed an approach to test data generation ( tdg ) by pe of clp @xcite and used it for tdgof bytecode . the approach is generic in that the same techniques can be applied to tdg other both low and high - level imperative languages . in figure [ fig : overview ] we overview the main two phases of this technique . in * phase i * , the input program written in some ( imperative ) language @xmath4 is compiled into an equivalent clp program @xmath5 . this compilation can be achieved by means of an ad - hoc decompiler ( e.g. , an ad - hoc decompiler of bytecode to prolog @xcite ) or , more interestingly , can be achieved automatically by relying on the first futamura projection by means of pe for logic programs as explained above ( e.g. , @xcite ) . now , the aim of * phase ii * is to generate test - cases which traverse as many different execution paths of @xmath6 as possible , according to a given coverage criteria . from this perspective , different test data will correspond to different execution paths . with this aim , rather than executing the program starting from different input values , the standard approach consists in performing _ symbolic execution _ such that a single symbolic run captures the behavior of ( infinitely ) many input values . the central idea in symbolic execution is to use constraint variables instead of actual input values and to capture the effects of computation using constraints . hence , the compilation from @xmath4 to clp allows us to use the standard clp execution mechanism to carry out this phase . in particular , by running the @xmath5 program without input values , each successful execution corresponds to a different computation path in @xmath6 .    rather than relying on the standard execution mechanism , we have proposed in @xcite to use pe of clp to carry out * phase ii*. essentially , we can rely on a clp partial evaluator which is able to solve the constraint system , in much the same way as a symbolic abstract machine would do . note that performing symbolic execution for tdgconsists in building a finite ( possibly unfinished ) evaluation tree by using a non - standard execution strategy which ensures both a certain coverage criterion and termination . this is exactly the problem that _ unfolding rules _ , used in partial evaluators of ( c)lp , solve . in essence , partial evaluators are non - standard interpreters which receive a set of partially instantiated atoms and evaluate them as determined by the so - called unfolding rule . thus , the role of the unfolding rule is to supervise the process of building finite ( possibly unfinished ) sld trees for the atoms . this view of tdgas a pe problem has important advantages . first , we can directly apply existing , powerful , unfolding rules developed in the context of pe . second , it is possible to explore additional abilities of partial evaluators in the context of tdg . in particular , the generation of a residual program from the evaluation tree returns a program which can be used as a _ test - case generator _ , i.e. , a clp program whose execution in clp returns further test - cases on demand without the need to start the tdgprocess from scratch . in the rest of the paper , we study the application of this general approach to tdgof prolog programs . as we have already mentioned , test data generation is about producing test - cases which traverse as many different execution paths as possible . from this perspective , different test data should correspond to different execution paths . thus , a main concern is to specify the computation paths for which we will produce test - cases . this requires first to determine the control flow of the considered language . in this section , we aim at defining the control flow of prolog programs that we will use for tdg . test data will be generated for the computation paths in the control flow . as usual a prolog program consists of a set of predicates , where each predicate is defined as a sequence of clauses of the form @xmath7 : - @xmath8 with @xmath9 . a predicate is univocally determined by its _ predicate signature _ @xmath10 , being @xmath11 the name of the predicate and @xmath12 its arity . throughout the rest of the paper we will consider prolog programs with the following features :    * rules are normalized , i.e. , arguments in the head of the rule are distinct variables . the corresponding bindings will appear explicitly in the body as unifications . * atoms appearing in the bodies of rules can be : unifications ( considered as builtins ) , calls to defined predicates , term checking builtins ( ` = = /2 ` , ` \==/2 ` , etc ) , and arithmetic builtins ( ` is/2 ` , ` < /2 ` , ` = < /2 ` , etc ) . other typical prolog builtins like ` fail/0 ` , ` ! /0 ` , ` if/3 ` , etc , have been deliberately left out to simplify the presentation . * all predicates must be moded and well - typed . we will assume the existence of a `` ` : - pred ` '' declaration associated with each predicate specifying the type expected for each argument ( see as example the declarations in fig . [ fig : cfgs ] ) . note that this assumption is sensible in the context of tdg(as the aim is the automatic generation of test _ input _ ) . also , it should not be a limitation as analyses that can automatically infer this information exist . the control flow in prolog programs is significantly more complex than in traditional imperative languages . the declarative semantics of prolog implies some additional features like : 1 ) several forms of backtracking , induced by the failure of a sub - goal , or by non - deterministic predicates ; or 2 ) forced control flow change by the predicate `` cut '' . traditionally , control - flow graphs ( cfgs for short ) are used to statically represent the control - flow of programs . typically , in a cfg , nodes are blocks containing a set of sequential instructions , and edges represent the flows that the program can follow w.r.t . the semantics of the corresponding programming language . in the literature , cfgs for prolog ( and mercury ) have been used for the aim of tdgin  @xcite ( @xcite for mercury ) . in particular , cfgs determine the computation paths for which test - cases will be produced . our framework relies on the cfgs of  @xcite which are known as _ p - flowgraph _ s . as will be explained later , there are some differences between these cfgs and the ones in @xcite which lead to different test - cases .    [ cols="^,^ " , ] figure  [ fig : cfgs ] depicts the prolog code together with the corresponding cfgs for predicates ` foo/2 ` and ` sorted/1 ` . predicate ` foo/2 ` , given a number in its first argument , returns , in the second one , the value ` pos ` if the number is positive and ` zero ` if it is zero . if the number is negative , it just fails . predicate ` sorted/1 ` , given a list of numbers , checks whether the list is strictly sorted , in that case it succeeds , otherwise it fails . the cfgs contain the following nodes :    * a non - terminal node associated to each atom in the body of each clause , * a set of terminal nodes `` t@xmath13 '' representing the success of the @xmath14-th clause , and * the terminal node `` f '' to represent failure . as regards edges , in principle all non - terminal nodes have two output flows , corresponding to the cases where the builtin or predicate call succeeds or fails respectively . they are labeled as `` yes '' or `` no '' for builtins ( including unifications ) , and as `` * * rs * * '' ( _ return - after - success _ ) or `` * * rf * * '' ( _ return - after - failure _ ) for predicate calls . there is an exception in the case of unifications where one of the arguments is a variable , in which case the unification can not fail . this can be known statically by using the mode information . see for example nodes `` ` z = pos ` '' and `` ` z = zero ` '' in the ` foo/2 ` cfg . both `` yes '' and `` * * rs * * '' edges point to the node representing the next atom in the clause or to the corresponding `` t@xmath13 '' node if the atom is the last one . finally , each `` t@xmath13 '' node has an output edge labeled as `` redo '' to represent the case in which the predicate is asked for more solutions . all `` no '' , `` * * rf * * '' and `` redo '' edges point either to the node corresponding to the first previous non - deterministic call in the same clause , or the first node of the following clause , or the `` f '' node if no node meets the above conditions . see as an example the `` * * rs * * '' and `` * * rf * * '' edges from the non - terminal node for sorted([y|r ] ) .      in order to define the computation paths determined by the cfgs , every edge in every cfg is labeled with a unique natural number . an special edge labeled with `` 0 '' and @xmath10 represents the entry of predicate @xmath10 . given the cfg for predicate @xmath1 , a _ computation sub - path _ is a sequence of numeric labels ( natural numbers ) @xmath15 s.t . :    * @xmath16 corresponds to either an entry , an `` * * rs * * '' , an `` * * rf * * '' or a `` redo '' edge , * @xmath17 leads to a terminal node or to a predicate call , and * for all consecutive labels @xmath18 , there exists a node corresponding to a builtin in the cfg of @xmath1 , for which @xmath19 is an input flow and @xmath20 is an output flow . given the cfgs corresponding to the set of predicates defining a program , a _ computation path _ ( cp for short ) for predicate @xmath11 is a concatenation @xmath21 ( @xmath22 ) of computation sub - paths such that :    * first label in @xmath23 is either @xmath24 , in which case we say it is a _ full _ cp , or corresponds to a `` redo '' edge , in which case we say it is a _ partial _ cp ( pcp for short ) . * last label in @xmath25 leads to a terminal node in the cfg of @xmath11 . if it is a @xmath0 node the cp is said to be _ successful _ otherwise it is called _ failing_. * for all @xmath26 whose last label leads to a node corresponding to a predicate call , @xmath27 , @xmath28 is a cp for the called predicate , and : * * if @xmath29 is successful then the first label in @xmath30 corresponds to an `` * * rs * * '' edge , * * otherwise ( @xmath29 is failing ) , it corresponds to an * rf * edge . * for all @xmath26 whose first label corresponds to a `` redo '' edge flowing from a `` t@xmath31 '' node in the cfg of predicate @xmath32 , @xmath33 , @xmath34 , whose first label corresponds either to an entry edge or to a `` redo '' edge flowing from `` t@xmath35 '' , @xmath36 , of the cfg of @xmath32 . if a cp contains at least one label corresponding to a `` redo '' flow , then the cp is said to be an _ after - retry _ cp . the rest of the cps are _ first - try _ cps . for example in ` foo/2 ` , @xmath37=@xmath38 and @xmath39=@xmath40 are first - try successful cps ; @xmath41=@xmath42 is a first - try failing branch ; @xmath43=@xmath44 is an after - retry successful cp ( although this one is unfeasible as @xmath45 and @xmath46 are disjoint conditions ) , and @xmath47=@xmath48 is an after - retry failing branch . in ` sorted/1 ` , @xmath49=@xmath50 is a first - try successful cp and @xmath51=@xmath52 is a first - try failing cp . it is interesting to observe the correspondence between the cps and the test data that make the program traverse them . in ` foo/2 ` , @xmath37 is followed by goal ` foo(1,z ) ` , @xmath39 by goal ` foo(0,z ) ` , @xmath41 by ` foo(-1,z ) ` , @xmath43 is an unfeasible path , and @xmath47 is followed by ` foo(0,z ) ` when we ask for more solutions . as regards ` sorted/1 ` , @xmath49 is followed by the goal ` sorted([0,1 ] ) ` and @xmath51 by ` sorted([0,1,0 ] ) ` . as we will see in sect . [ sec : gener - test - cases ] , these will become part of the test - cases that we automatically infer . a key feature of our cfgs is that they make explicit the fact that after failing with a clause the computation has to re - try with the following clause , unless a non - deterministic call is left behind . e.g. , in ` foo/2 ` the cfg makes explicit that the only way to get a first - try failing branch is through the cp @xmath53 , hence traversing , and failing in , both conditions @xmath45 and @xmath46 . therefore , a test data to obtain such a behavior will be a negative number for argument @xmath54 . other approaches , like the one in  @xcite , do not handle flows after failure in the same way . in fact , in  @xcite , edge `` 3 '' in ` foo/2 ` goes directly to node `` f '' . it is not clear if these approaches are able to obtain such a test data . as another difference with previous approaches to tdgof prolog , we want to highlight that we use cfgs just to reason about the program transformation that will be presented in the following section and , in particular , to clarify which features we want to capture . however , in previous approaches , test - cases are deduced directly from the cfgs . as we outlined in sect . [ sec : intro ] , an intrinsic feature of the second phase of our approach is that it can only produce results associated to non - failing derivations . this is the main reason why the general approach to tdg by pe sketched in sect . [ sec : basics - tdg - partial ] is directly applicable only to tdg of imperative languages . to enable its application to prolog , we propose a program transformation which makes failure explicit in the prolog program . the specialisation of meta - programs has been proved to have a large number of interesting applications@xcite . futamura projection s to derive compiled code , compilers and compiler generators fall into this category . the specialization of meta - interpreters for non - standard computation rules has also been studied . furthermore , language extensions and enhancements can be easily expressed as meta - interpreters which perform additional operations to the standard computation . in short , program specialisation offers a general compilation technique for the wide variety of procedural interpretations of logic programs . among them , we propose to carry out our transformation which makes failure in logic programs explicit by partially evaluating a prolog meta - interpreter which captures failing derivations w.r.t . the original program . first , in sect .  [ sec : interpreter ] we describe such a meta - interpreter emphasizing the prolog control features which we want to capture . then , sect . [ sec : control_pe ] describes the control strategies which have to be used in pe in order to produce an effective transformation .      given a prolog program and given a goal , our aim is to define an interpreter in which the computation of the program and goal produces the same results as the ones obtained by using the standard prolog computation but with the difference that failure is never reported . instead , an additional argument @xmath55 will be bound to the value `` yes '' , if the computation corresponds to a successful derivation , and to `` no '' if it corresponds to a failing derivation . predicate ` solve/4 ` is the main predicate of our meta - interpreter whose first and second arguments are the predicate signature and arguments of the goal to be executed ; and its third argument is the answer ; by now we ignore the last argument . for instance , the call ` solve(foo/2,[0,z],answer , _ ) ` succeeds with @xmath56 and @xmath57 , and ` solve(foo/2,[-1,z],answer , _ ) ` also succeeds , but with @xmath58 . the interpreter has to handle the following issues :    1 . the prolog _ backtracking _ mechanism has to be explicitly implemented . to this aim , a stack of _ choice points _ is carried along during the computation so that : * if the derivation fails : ( 1 ) when the stack is empty , it ends up with success and returns the value `` no '' , ( 2 ) otherwise , the computation is resumed from the last choice point , if any ; * if it successfully ends : ( 1 ) when the stack is empty , the computation finishes with answer `` yes '' , ( 2 ) otherwise , the computation is resumed from the last choice point . 2 .   when backtracking occurs , all variable bindings , between the current point and the choice point to resume from , have to be undone . 3 .   the interpreter has to be implemented in a _ big - step _ fashion . this is a requirement for obtaining an effective decompilation . more details are given in sect . [ sec : control_pe ] .    .... solve(p / ar , args , answer , tncps ) : -     pred(p / ar , _ ) ,     build_s0(p / ar , args , s0,outvs ) ,     exec(args , s0,sf ) ,     sf = st(_,_,_,outvs',answer , tncps/ _ ) ,     outvs ' = outvs . exec(_,s , sf ) : -      s = st(_,[],[],outvs , yes , ncps ) ,     sf = st(_,_,_,outvs , yes , ncps ) . exec(_,s , sf ) : -      s = st(_,[],[_|_],outvs , yes , ncps ) ,     sf = st(_,_,_,outvs , yes , ncps ) . exec(_,s , sf ) : -      s = st(_,_,[],outvs , no , tncps/0 ) ,     sf = st(_,_,_,outvs , no , tncps/0 ) . exec(args , s , sf ) : -      s = st(_,[],[cp|cps],_,yes , tncps/0 ) ,     build_retry_state(args , cp , cps , tncps , s ' ) ,     exec(args , exec(args , s , sf ) : -      s = st(_,_,[cp|cps],_,no , tncps/0 ) ,     build_retry_state(args , cp , cps , tncps , s ' ) ,     exec(args , s',sf ) . ....       .... exec(args , s , sf ) : -     s = st(pp,[a|as],cps , outvs , yes , tncps / encps ) ,     pp = pp(p / ar , clid , pt ) ,     internal(a ) ,     functor(a , a_f , a_ar ) ,     a = .. [ a_f|a_args ] ,     next(pt , pt ' ) ,     solve(a_f / a_ar , a_args , ans , encps ' ) ,     tncps ' is tncps + encps ' ,      encps '' is encps + encps ' ,     pp ' = pp(p / ar , clid , pt ' ) ,     s ' = st(pp',as , cps , outvs , ans , tncps'/encps '' ) ,     exec(args , s',sf ) . exec(args , s , sf ) : -     s = st(pp,[a|as],cps , outvs , yes , ncps ) ,     pp = pp(p / ar , clid , pt ) ,     builtin(a ) ,     next(pt , pt ' ) ,     run_builtin(pp , a , ans ) ,     pp ' = pp(p / ar , clid , pt ' ) ,     s ' = st(pp',as , cps , outvs , ans , ncps ) ,     exec(args , s',sf ) . ....    figure  [ fig : interpreter ] shows an implementation of a meta - interpreter which handles the above issues . the fourth argument of the main predicate ` solve/4 ` , named ` tncps ` , contains upon success the total number of choice points not yet considered , whose role will be explained later . the interpreter assumes that the program is represented as a set of ` pred/2 ` and ` clause/3 ` facts . there is a ` pred/2 ` fact per predicate providing its predicate signature , number of clauses and mode information ; and a ` clause/3 ` fact per clause providing the actual code and clause identifier . predicate ` solve/4 ` basically builds an initial state on ` s0 ` , by calling ` build_s0/4 ` , and then delegates on ` exec/3 ` to obtain the final state ` sf ` of the computation . the output information , ` outvs ` , is taken from ` sf ` . the state carried along is of the form ` st(pp , g , cps , outvs , ans , ncps ) ` , where ` pp ` is the current program point , ` g ` the current goal , ` cps ` is the stack of choice points ( list of program points ) , ` outvs ` the list of variables in ` g ` corresponding to the output parameters of the original goal , ` ans ` the current answer ( `` yes '' or `` no '' ) and ` ncps ` the number of choice points left behind . a program point is of the form ` pp(p / ar , clid , pt ) ` , where ` p / ar ` , ` clid ` and ` pt ` are the predicate signature , the clause identifier and the program point of the clause at hand . predicate ` exec/3 ` implements the main loop of the interpreter . given the current state in its second argument it produces the final state of the computation in the third one . it is defined by the seven clauses which are applied in they following situations :    @xmath59 : :    _ the current goal is empty , the answer `` yes '' and there are no    pending choice points . _ then , the computation finishes with answer    `` yes '' . the current answer is actually used as a flag to indicate    whether the previous step in the computation succeeded or failed ( see    the last two ` exec/3 ` clauses ) . @xmath60 : :    _ as @xmath59 but having at least one choice point . _    this clause represents the solution in which the computation ends . the    4@xmath61 clause takes the other alternatives . @xmath62 : :    _ the previous step failed and there are no pending choice points_.    then , the computation ends with answer `` no '' . @xmath63 : :    _ the current goal is empty , the answer `` yes '' and there is at least    one pending choice point . _ this is the same situation as in the    @xmath64 clause , however in this case the alternative of    resuming from the last choice point is taken . the corresponding state    ` s ` is built by means of ` build_retry_state/5 ` and the computation is    resumed from ` s ` by recursively calling ` exec/3 ` . @xmath65 : :    _ the previous step failed and there is at least one pending choice    point . _ then , the computation is resumed from the last choice point in    the same way as in the previous clause . @xmath66 : :    _ the first atom to be solved is user - defined . _ a call to ` solve/4 `    handles the atom , and the computation proceeds with the next program    point of the same clause which was the current one before calling    ` solve/4 ` . this way of solving a predicate call makes the interpreter    _ big - step _ ( issue ( 3 ) above ) . @xmath67 : :    _ the first atom to be solved is a builtin . _ then , ` run_builtin/3 `    produces the corresponding answer , and the computation proceeds with    the following program point . an interesting observation ( also    applicable for the previous clause ) is that the answer obtained from    ` run_builtin/3 ` ( or ` solve/4 ` ) is now set up as the answer of the next    state . this will make the computation go through the    3@xmath68 or 5@xmath61 clauses in the following    step , if the obtained answer was `` no '' . the correspondence between these clauses and the flows in the cfgs is as follows : clauses @xmath69 , @xmath64 and @xmath70 represent the output edges from every `` t '' node . clause @xmath71 represents the `` no '' edges to `` f '' nodes and @xmath72 the `` no '' edges to non - terminal nodes . finally clauses @xmath73 and @xmath74 represents the execution of builtins and predicate calls in non - terminal nodes and their corresponding `` yes '' edges . let us now explain how the interpreter handles the above three issues . to handle ( 1 ) , a stack of choice points is carried along within the state , initialised to contain all initial program points of each clause defining the predicate to be solved , except for the first one . e.g. , the initial stack of choice points for ` sorted/1 ` is ` [ pp(sorted/1,2,1),pp(sorted/1,3,1 ) ] ` . how this stack is used to perform the backtracking is already explained in the description of the 4@xmath61 and 5@xmath61 ` exec/3 ` clauses above . as regards issue ( 2 ) , a quite simple way to implement this in prolog is to produce the necessary fresh variables every time the computation is resumed . this is done inside ` build_retry_state/5 ` . the corresponding unification to link the fresh variables with the original goal variables is made at the end ( see last line of ` solve/4 ` ) . this is the reason why 1 ) the list of the actual variables used in the current goal needs to be carried along within the state ; and 2 ) the original arguments are carried along as the first argument of ` exec/3 ` , as the original ground arguments provided , have to be used when resuming from a choice point . finally , it is worth mentioning that ` solve/4 ` does not return the actual stack of choice points but only the number of them . this means that during a computation the interpreter only considers choice points of the predicate being solved . the question is then , how can the interpreter backtrack to the last choice point , including those induced by other computations of ` solve/4 ` ? e.g. , how can the interpreter follow edge `` 13 '' in the cfg of ` sorted/1 ` ? the interpreter performs the backtracking in the following way : 1 ) the total number of choice points left behind , ` tncps ` , is carried along within the state and finally returned in the last argument of ` solve/4 ` . 2 ) the number of choice points corresponding to invoked predicates , ` encps ` , is also carried along . it is updated right after the call to ` solve/4 ` in the 6@xmath61 clause of ` exec/3 ` . both numbers are stored in the last argument of the state as ` tncps / encps ` . 3 ) execution is resumed from choice points of the current predicate only if @xmath75 , as it can be seen in the 4@xmath61 and 5@xmath61 clauses . otherwise , the computation just fails and prolog s backtracking mechanism is used to ask the last invoked predicate for more solutions . this indeed means that the non - determinism of the program is still implicit . the specialisation of interpreters has been studied in many different contexts , see e.g.  @xcite . very recently , @xcite proposed control strategies to successfully specialise low - level code interpreters w.r.t . non trivial programs . here we demonstrate how such guidelines can be , and should be , used in the specialisation of non - trivial prolog meta - interpreters . they include :    1 . _ big - step _ interpreter . this solves the problem of handling recursion ( see  @xcite ) and enables a compositional specialisation w.r.t . the program procedures ( or predicates ) . note that an effective treatment of recursion is specially important in prolog programs where recursion is heavily used . optimality _ issues . optimality must ensure that : a ) the code to be transformed is traversed exactly once , and b ) residual code is emitted once in the transformed program . to achieve optimality , during unfolding , all atoms corresponding with _ divergence _ or _ convergence points _ in the cfg of the program to be transformed , has to be _ memoised _ ( see sect .  [ sec : pe - basics ] ) . a divergence ( convergence ) point is a program point from ( to ) which two or more flows originate ( converge ) . we already explained that the interpreter in fig . [ fig : interpreter ] is big - step . as regards optimality , by looking at the cfgs of fig . [ fig : cfgs ] , we can observe : 1 ) all program points are divergence points except those corresponding with unifications in which one argument is a variable , and 2 ) the first program point of every clause , except for the one of the first clause , is a convergence point . we assume that and denote , respectively , the set of convergence points and divergence points of a predicate . we follow the syntax of  @xcite for pe annotations . an annotation is of the form `` @xmath76 \rightarrow ann ~pred$ ] '' where @xmath77 is an optional precondition defined as a logic formula , @xmath78 is the kind of annotation ( only * memo * in this case ) , and @xmath79 is a predicate descriptor , i.e. , a predicate function and distinct free variables . then , to achieve an effective transformation , we specialise the interpreter in fig .  [ fig : interpreter ] w.r.t . the program to be transformed by using the following annotation for each predicate ` p / ar ` in the program : @xmath80 additionally ` solve/4 ` and ` run_builtin/3 ` are also annotated to be memoised always to avoid code duplications . this already describes how the specialisation has to be steered in the local control . as regards the global control , the only predicate which can introduce non - termination is ` exec/3 ` . its first and third arguments contain a fixed structure with variables . the second one might be problematic as it ranges over the set of all computable states at specialisation time . note that the number of computable states remains finite thanks to the big - step nature of the interpreter . still , it can happen that the same program point is reached with different values for the ` ncps ` sub - term of the state . therefore , if one wants to achieve the optimality criterion above , such argument has to be always generalised in global control . figure  [ fig : transformed ] depicts the transformed code we obtain for predicate ` foo/2 ` . it can be observed that there is a clear correspondence between the transformed code and the cfg in fig . [ fig : cfgs ] . thus , predicate ` solve/4 ` represents the node `` ` x>0 ` '' , ` exec_1/5 ` implements its continuation , whose three clauses correspond to the three sub - paths @xmath81 , @xmath82 and @xmath83 respectively . predicate ` exec_2/4 ` represents the node `` ` x=0 ` '' and ` exec_3/5 ` implements its continuation , whose two clauses correspond to the sub - paths @xmath84 and @xmath85 . note that edge `` 8 '' is not considered in the meta - interpreter ( nor in the transformed program ) as it is meaningless for tdg . it is worth mentioning that the transformed program captures the way in which variable bindings are undone . for instance in ` solve(foo/2,[c , d],\ldots ) ` , if we keep track of variables ` c ` and ` d ` , it can be seen that ` d ` , which corresponds to variable ` z ` in the original code , is only used for the final unification ` f=[d ] ` , while new fresh variables are used for the unifications with ` pos ` and ` zero ` . however , variable ` c ` , which corresponds to variable ` x ` in the original code , is actually used for the checks in ` run_builtin_1/2 ` and ` run_builtin_2/2 ` . this turns out to be fundamental when trying to obtain test data associated to the _ first - try failing _ . it must be the same variable the one which , at the same time , is not `` @xmath86 '' and not `` = 0 '' . otherwise we can not obtain a negative number as test data for such cp . finally , observe that the original prolog arithmetic builtins have been ( automatically ) transformed into their ` clpfd ` counterparts . c|c    .... solve(foo/2,[c , d],a , b ) : -     run_builtin_1(e , c ) ,     exec_1(c , e , f , a , b ) , f = [ d ] . exec_1(a , no , f , g , h ) : - exec_2(a , f , g , h ) . exec_1(_,yes,[pos],yes,1 ) . exec_1(a , yes , f , g , h ) : - exec_2(a , f , g , h ) . exec_2(a , g , h , i ) : -     run_builtin_2(k , a ) , exec_3(k , g , h , i ) . ....    &    .... exec_3(no,[_],no,0 ) . exec_3(yes,[zero],yes,0 ) . run_builtin_1(yes , a ) : - a#>0 . run_builtin_1(no , a ) : - \+ a#>0 .    run_builtin_2(yes , a ) : - a#=0 . run_builtin_2(no , a ) : - \+ a#=0 . .... once the original prolog program has been transformed into an equivalent prolog program with explicit failure , we can use the approach of @xcite to carry out * phase ii * ( see fig .  [ fig : overview ] ) and generate test data both for successful and failing derivations . as we have explained in sect . [ sec : general - scheme ] , the idea is to perform a second pe over the clp transformed program where the unfolding rule plays the role of the coverage criterion . in @xcite an unfolding rule implementing the _ block - count(k ) _ coverage criterion was proposed . a set of computation paths satisfies the _ block - count@xmath87 criterion _ if it includes all terminating computation paths which can be built in which the number of times each block is visited does not exceed the given @xmath88 . the blocks the criterion refers to are the blocks or nodes in the cfgs of the original prolog program . as the only form of loops in prolog are recursive calls , the `` @xmath88 '' in the _ block - count@xmath87 _ actually corresponds to the number of recursive calls which are allowed . unfortunately , the presence of prolog s negation in our transformed programs complicates this phase . the negation will appear in the transformed program for `` no '' branches originating from nodes corresponding to a ( possibly ) failing builtin . see for example predicates ` run_builtin_1/3 ` and ` run_builtin_2/3 ` in the transformed code of ` foo/2 ` in fig . [ fig : transformed ] . while prolog s negation works well for ground arguments , it gives no information for free variables , as it is required in the evaluation performed during this tdg phase . in particular , in the ` foo/2 ` example , given the computation which traverses the calls `` ` \+ a#>0 ` '' and `` ` \+ a#=0 ` '' ( corresponding to the path @xmath89 in the cfg ) , we need to infer that `` ` a<0 ` '' . in other words , we need somehow to turn the _ negative _ information into _ positive _ information . this transformation is straightforward for arithmetic builtins : we just have to replace `` ` \+ e_1#=e_2 ` '' by `` ` e_1#\=e_2 ` '' and `` ` \+ e_1#>e_2 ` '' by `` ` e_1#=<e_2 ` '' , etc . this transformation allows us to obtain the following set of test - cases for ` foo/2 ` : @xmath90,[pos],yes / first - try}\rangle , &   \langle\mbox{\tt [ 1],[\_],no / after - retry}\rangle , \\ \langle\mbox{\tt [ 0],[zero],yes / first - try}\rangle , & \langle\mbox{\tt [ -100],[\_],no / first - retry}\rangle \end{array}\right\}\ ] ]    they correspond respectively ( reading by rows ) to the cps @xmath91 , @xmath92 , @xmath40 and @xmath42 . each test - case is represented as a 3-tuple @xmath93 being @xmath94 the list of input arguments , @xmath95 the list of output arguments and @xmath96 the answer . the answer takes the form @xmath97 with @xmath98 and @xmath99 , we decided not include in the interpreter the support to calculate the ` first - try / after - retry ` value . ] , so that we obtain sufficient information about the kind of cp to which the test - case corresponds ( see sect . [ sec : control_flow ] ) . as there are no recursive calls in ` foo/2 ` such test - cases are obtained using the _ block - count@xmath87 _ criterion for any @xmath88 ( greater than @xmath24 ) . the domain used for the integer number is @xmath100 . however , it can be the case that negation involves unifications with symbolic data . for example , the transformed code for ` sorted/1 ` includes the negations `` ` \+ l= [ ] ` '' and `` ` \+ l= [ _ _ ] ` '' . as before , we might write transformations for the negated unifications involving lists , so that at the end it is inferred that `` ` l= [ _ , _ _ ] ` '' . however this would be too an ad - hoc solution as many distinct term structures , different from lists , can appear on negated unifications . a solution for this problem has been recently proposed for mercury in the same context @xcite . it roughly consists in the following : 1 ) it is assumed that each predicate argument is well - typed . 2 ) a domain is initialised for each variable , containing the set of possible functors the variable can take . 3 ) when a negated unification involving an output variable is found ( in their terminology a negated _ decomposition _ ) , the corresponding functor is removed from the variable domain . it is crucial at this point the assumption that complex unifications are broken down into simple ones . 4 ) finally , a search algorithm is described to generate particular values from the type definition and final domain for the variable . the technique is implemented using chr and can be directly used in principle for our purposes as well .    on the other hand , advanced declarative languages like toy  @xcite make possible the co - existence of different constraint domains . in particular , the co - existence of boolean and numeric constraint domains enables the possibility of using _ disequalities _ involving both symbolic data and numbers . this allows for example expressing the negated unifications `` ` \+ l= [ ] ` '' and `` ` \+ l= [ _ _ ] ` '' as disequality constraints `` ` l/= [ ] ` '' and `` ` l/= [ _ _ ] ` '' . additionally , by relying on the boolean constraint solver , the negated arithmetic builtins `` ` \+ a#>0 ` '' and `` ` \+ a#=0 ` '' can be encoded as `` ` ( a#>0 ) = = false ` '' and `` ` ( a#=0 ) = = false ` '' . this is in principle a more general solution that we want to explore , although a thorough experimental evaluation needs to be carried out to demonstrate its applicability to our particular context . now , by using any of the techniques outlined above , we obtain the following set of test - cases for ` sorted/1 ` , using _ block - count@xmath101 _ as the coverage criterion : @xmath102,[],yes / first - try}\rangle , &   \langle\mbox{\tt [ [ 0]],[],yes / first - try}\rangle,\\ \langle\mbox{\tt [ [ 0,1]],[],yes / first - try}\rangle , & \langle\mbox{\tt [ [ 0,1,2]],[],yes / first - try}\rangle,\\ \langle\mbox{\tt [ [ 0,1,2,0\textbar\_]],[],no / first - try}\rangle , & \langle\mbox{\tt [ [ 0,1,0\textbar\_]],[],no / first - try}\rangle,\\ \langle\mbox{\tt [ [ 0,0\textbar\_]],[],no / first - try}\rangle \end{array}\right\}\ ] ] they correspond respectively ( reading by rows ) to the cps `` @xmath103 '' , `` @xmath104 '' , `` @xmath105 '' , `` @xmath106 '' , `` @xmath107 '' , `` @xmath108 '' , `` @xmath109 '' . they are indeed all the paths that can be followed with no more than @xmath110 recursive calls . this time the domain has been set up to @xmath111 . very recently , we proposed in  @xcite a generic approach to tdg by pe which in principle can be used for any imperative language . however , applying this approach to tdg of a declarative language like prolog introduces some difficulties like the handling of failing derivations and of symbolic data . in this work , we have sketched solutions to overcome such difficulties . in particular , we have proposed a program transformation , based on pe , to make failure explicit in the prolog programs . to handle prolog s negation in the transformed programs , we have outlined existing solutions that make it possible to turn the negative information into positive information . though our preliminary experiments already suggest that the approach can be very useful to generate test - cases for prolog , we plan to carry out a thorough practical assessment . this requires to cover additional prolog features like the module system , builtins like ` cut/0 ` , ` fail/0 ` , ` if/3 ` , etc . and also to compare the results with other tdg systems . we also want to study the integration of other kinds of coverage criteria like _ data - flow _ based criteria . finally , we would like to explore the use of static analyses in the context of tdg . for instance , the information inferred by a _ failure analysis _ can be very useful to prune some of the branches that our transformed programs have to consider . this work was funded in part by the information society technologies program of the european commission , future and emerging technologies under the ist-15905 _ mobius _ project , by the spanish ministry of education under the tin-2005 - 09207 _ merit _ project , and by the madrid regional government under the s-0505/tic/0407 _ promesas _ project . e.  albert , m.  gmez - zamalloa , and g.  puebla . est data generation of bytecode by clp partial evaluation . in _ 18th international symposium on logic - based program synthesis and transformation ( lopstr08 ) _ , lncs . springer - verlag , july 2008 . to appear . f.  degrave , t.  schrijvers , and w.  vanhoof . automatic generation of test inputs for mercury . in _ 18th international symposium on logic - based program synthesis and transformation ( lopstr08 ) _ , lncs . springer - verlag , 2008 . to appear . m.  gmez - zamalloa , e.  albert , and g.  puebla . odular decompilation of low - level code by partial evaluation . in _ 8th international working conference on source code analysis and manipulation ( scam08)_. ieee computer society , september 2008 . to appear . kim  s. henriksen and john  p. gallagher . abstract interpretation of pic programs through logic programming . in _ scam 06 : proceedings of the sixth ieee international workshop on source code analysis and manipulation _ , pages 184196 . ieee computer society , 2006 . g.  luo , g.  bochmann , b.  sarikaya , and m.  boyer . control - flow based testing of prolog programs . in _ in proc . of the 3rd international symposium on software reliability engineering _ , pages 104113 , 1992 . m.  mndez - lojo , j.  navas , and m.  hermenegildo . lexible ( c)lp - based approach to the analysis of object - oriented programs . in _ 17th international symposium on logic - based program synthesis and transformation ( lopstr07 ) _ , august 2007 .
in recent work , we have proposed an approach to test data generation ( tdg ) of imperative bytecode by _ partial evaluation _ ( pe ) of clp which consists in two phases : ( 1 ) the bytecode program is first transformed into an equivalent clp program by means of interpretive compilation by pe , ( 2 ) a second pe is performed in order to supervise the generation of test - cases by execution of the clp decompiled program . 
 the main advantages of tdgby pe include flexibility to handle new coverage criteria , the possibility to obtain test - case generators and its simplicity to be implemented . 
 the approach in principle can be directly applied for tdgof any imperative language . however , when one tries to apply it to a declarative language like prolog , we have found as a main difficulty the generation of test - cases which cover the more complex control flow of prolog . 
 essentially , the problem is that an intrinsic feature of pe is that it only computes non - failing derivations while in tdgfor prolog it is essential to generate test - cases associated to failing computations . 
 basically , we propose to transform the original prolog program into an equivalent prolog program with _ 
 explicit failure _ by partially evaluating a prolog interpreter which captures failing derivations w.r.t . 
 the input program . 
 another issue that we discuss in the paper is that , while in the case of bytecode the underlying constraint domain only manipulates integers , in prolog it should properly handle the symbolic data manipulated by the program . 
 the resulting scheme is of interest for bringing the advantages which are inherent in tdgby pe to the field of logic programming .