A Method for Compiling and Executing Expressive Assertions

A Method for Compiling and Executing Expressive Assertions F.J. Gal´an Morillo and J.M. Ca˜nete Valde´on Dept. of Languages and Computer Systems. Faculty of Computer Science of Seville Av. Reina Mercedes s/n 41012 Sevilla, Spain. phone: (34) 95 455 27 73, fax: (34) 95 455 71 39 {galanm,canete}@lsi.us.es Abstract. Programming with assertions constitutes an effective tool to detect and correct programming errors. The ability of executing formal specifications is essential in order to test automatically a program with respect to its assertions. However, formal specifications may describe recursive models which are difficult to identify so current assertion checkers limit, in a considerable way, the expressivity of the assertion language. In this paper, we are interested in showing how transformational synthesis can help to execute “expressive” assertions of the form ∀x(r(x)⇔QyR(x, y)) where xis a set of variables to be instantiated at execution time, Qis an existential or universal quantifier and Ra quantifier free formula in the language of a particular first-order theory Awe call assertion context. The class of assertion contexts is interesting because it presents a balance between expressiveness for writing assertions and existence of effective methods for executing them by means of synthesized (definite) logic programs. Keywords: Assertion, correctness, formal specification, logic program, program synthesis, programming with assertions, meaning-preserving transformation, testing. 1 Introduction Experience has shown that writing assertions while programming is an effective way to detect and correct programming errors. As an added benefit, assertions serve to document programs, enhancing maintainability. Programming languages such as Eiffel [18], SPARK [2] and recent extensions to the Java programming language, such as iContract [13], JML [16] and Jass [5], allow to write assertions into the program code in the form of pre-post conditions and invariants. Software components called assertion checkers are then used to decide if program assertions hold at execution time. However, and due to mechanization problems, current checkers do not accept the occurrence of unbounded quantification in assertions. This fact limits the expressivity of the assertion language and so the effectiveness of testing activities by means of runtime assertion checkers. In order to motivate the problem, we show in Ex. 1 a (schematic) program which includes an unbounded quantified sub-formula in its post-condition. Example 1. A program which returns a number different to zero if and only if the parameter lis a subset of the parameter s. Program types Nat and Set are used to represent natural numbers and sets of natural numbers respectively. subset(l:Set,s:Set) return z:Nat pre: true ... program code ... post: ¬idnat(z,0) ⇔∀e(member(e, l)⇒member(e, s)) where idnat is the identity relation for natural numbers: idnat :Nat×Nat idnat(0,0) ⇔true ∀x(idnat(s(x),0) ⇔false) ∀y(idnat(0,s(y)) ⇔false) ∀x, y(idnat(s(x),s(y)) ⇔idnat(x, y)) where member is a relation to decide if a natural number is included or not in a set: member :Nat×Set ∀e(member(e, [])⇔false) ∀e(member(e, [x|y]) ⇔(idnat(x, e)∨member(e, y))) At execution time, subset’s program code will supply values (ground terms) to assertion variables l,sand zclosing their interpretations. Thus, the correctness of a program behavior such as subset([s(0)],[0,s(0)]) = s(0) will depend on the evaluation of ¬idnat(s(0),0) ⇔∀e(member(e, [s(0)]) ⇒member(e, [0,s(0)])) (i.e. subset’s post-condition after substituting l,sand zby values [s(0)], [s(0),0] and s(0) respectively). Due to the form of idnat’s axioms, it is not difficult to find a program able to evaluate ground atoms such as idnat(s(0),0), in fact, the if-part of idnat’s axioms can be considered one of such programs (Ex. 2). However, the occurrence of unbounded quantification in sub-formulas such as ∀e(member(e, [s(0)]) ⇒member(e, [0,s(0)])) complicates extraordinarily the search for such programs [9]. Due to this fact, current assertion checkers [18], [2], [5], [13], [16] does not consider the use of unbounded quantification in their assertion languages. Such a decision limits the expressivity of the assertion language and, therefore, the effectiveness of testing activities by means of runtime assertion checkers. Example 2. A logic program which is able to evaluate ground atoms for idnat. idnat(0,0) ⇐ idnat(s(x),s(y)) ⇐idnat(x, y) Our objective can be summarized in the following questions: 1. Is it possible to extend current checkers to execute “expressive assertions”? Firstly, we need to formalize what we call ”expressive assertions”. For us, an expressive assertion is a (new) relation rwhich represents a quantified sub-formula QyR(x, y) within a program assertion. Formally, ris defined by means of one axiom of the form ∀x(r(x)⇔QyR(x, y)) where xis a set of variables to be instantiated at execution time, Qis an existential or universal quantifier, and Ra quantifier free formula in the language of a particular first order theory Acalled assertion context. For instance, ∀l, s(r(l,s)⇔ ∀e(member(e, l)⇒member(e, s))) is the definition of an expressive assertion rfor the quantified sub-formula ∀e(member(e, l)⇒member(e, s)) in subset’s post-condition (Ex. 1). Therefore, to answer “yes” to the question is equivalent to say that assertion checkers must be able to evaluate any ground atom r(t)inAwhere tis the set of values supplied by the program at execution time. 2. How can we do it? Logic program synthesis constitutes an important aid in order to overcome the problem. Our intention is: –If Q=∃, to synthesize a (definite) logic program r∃ 1of the form r∃ 1(x, y) ⇐P∃(x, y) from a specification of the form ∀x, y(r∃ 1(x, y)⇔R(x, y)). –If Q=∀, to synthesize a (definite) logic program r∀ 1of the form r∀ 1(x, y) ⇐P∀(x, y) from a specification of the ∀x, y(r∀ 1(x, y)⇔¬R(x, y)). In any case, synthesized programs rQ 1must be totally correct wrt goals of the form ⇐rQ 1(t, y). In order to synthesize logic programs, we have studied some of the most relevant synthesis paradigms (constructive, transformational and inductive) [7,8,9]. In particular, we are interested in transformational methods [4,14] however, some important problems are exposed in [6,8]: “A transformation usually involves a sequence of unfolding steps, then some rewriting, and finally a folding step. The eureka about when and how to define a new predicate is difficult to find automatically. It is also hard when to stop unfolding. There is a need for loop-detection techniques to avoid infinite synthesis through symmetric transformations”. In order to overcome these problems, we propose to develop program synthesis within assertion contexts [11]. Such a decision will allow us: –To structure the search space for new predicates. –To define a relation of similarity on formulas for deciding when to define new predicates and, from here, a particular folding rule to define new predicates without human intervention. –To define an incremental compilation method where no symmetric transformations are possible. 3. How can assertion checkers evaluate ground atoms r(t)from goals ⇐rQ 1(t, y) in a refutation system such as Prolog? –The execution of ⇐r∃ 1(t, y) in a Prolog system will compute a set of substitutions {θ1, ..., θj}for y, thus: If {θ1, ..., θj}=∅, by total correctness of r∃ 1,A¬r(t) else Ar(t). –The execution of ⇐r∀ 1(t, y) in a Prolog system will compute a set of substitutions {θ1, ..., θj}for y, thus: If {θ1, ..., θj}=∅, by total correctness of r∀ 1,Ar(t) else A¬r(t). Our work is explained in the following manner. In Sect(s). 2 and 3 we introduce a set of preliminary definitions and a brief background on transformational synthesis respectively. Section 4 formalizes assertion contexts as a class of particular first-order theories to write expressive assertions. Then, Sect. 5 defines a compilation method for expressive assertions. Section 6 explains how to execute expressive assertions from compilation results. Finally, we conclude in Sect. 7. 2 Preliminary Definitions This section introduces a set of preliminary definitions in order to clarify the vocabulary we will use in the rest of the paper. Definition 1 (Term, Formula). A term of type τis defined inductively as follows: (a) a variable of type τis a term of type τ, (b) a constant of type τis a term of type τ, and (c) if fis an n-ary function symbol of type τ1, ..., τn→τ and tiis a term of type τi(i=1..n), then f(t1, ..., fn)is a term of type τ. A formula is defined inductively as follows: (a) if ris a relation symbol of type τ1, ..., τnand tiis a term of type τi(i=1..n), then r(t1, ..., tn)is a typed atomic formula (or simply an atom), (b) if Fand Gare typed formulas, then so are ¬F,F∧G,F∨G,F⇒Gand F⇔Gand (c) if Fis a typed formula and xis a variable of type τ, then ∀τxF and ∃τxF are typed formulas (for legibility reasons we will omit subscripts in quantifiers). A typed literal is a typed atom or the negation of a typed atom. A ground term (or value) is a term not containing variables. Similarly, a ground formula is a formula not containing variables. A closed formula is a formula whose variables are quantified. A quantifier-free formula is a formula without quantifiers. Definition 2 (Herbrand base). The Herbrand universe of a first order language Lis the set of all ground terms, which can be formed out of the constants and function symbols appearing in L. The Herbrand base for Lis the set of all ground atoms which can be formed by using relation symbols from Lwith ground terms from the Herbrand universe of L. Definition 3 (Patterns). A term pattern tPis obtained from a term tby replacing each variable occurrence in tby the symbol . An atom pattern r(t)P is obtained from an atom r(t)by replacing every term occurrence in r(t)by its respective term pattern. We say that lPis a literal pattern for r(t)if either lP=r(t)Por lP=¬r(t)P. A formula pattern FPis obtained from a quantifierfree formula Fby replacing every literal in Fby its respective literal pattern. We say that t1P>t 2Pif either t1P=and t2P=f(t2,1P, ..., t2,nP) or t1P=f(t1,1P, ..., t1,nP)and t2P=f(t2,1P, ..., t2,nP)and there exists a nonempty subset S⊆{1..n}such that t1,iP>t 2,iPfor every i∈Sand t1,j P=t2,jP for every j∈({1..n}−S). Let r(t1,1, ..., t1,n)Pand r(t2,1, ..., t2,n)Pbe two atom patterns, we say that r(t1,1, ..., t1,n)P>r(t2,1, ..., t2,n)Pif there exists a non-empty set S⊆{1..n}such that t1,iP>t 2,iPfor every i∈Sand t1,j P=t2,jPfor every j∈({1..n}−S). Definition 4 (Definite Logic Program, Definite Goal). A definite logic clause is a universally closed formula of the form A⇐B1, ..., Bnwhere A,B1, ..., Bnare atoms. A definite logic program is a finite set of definite program clauses (Ex. 2 shows a definite logic program). A definite goal is a clause of the form ⇐B1, ..., Bn. 3 Background on Transformational Synthesis In transformational synthesis, a sequence of meaning preserving transformation rules is applied to a specification until a program is obtained [8]. This kind of stepwise forward reasoning is feasible with axiomatic specifications of the form ∀x(r(x)⇔R(x)). There are atomic transformation rules such as unfolding (replacing an atom by its definition), folding (replacing a sub-formula by an atom) and rewrite and simplification rules. The objective of applying transformations is to filter out a new version of the specification where recursion may be introduced by a folding step. This usually involves a sequence of unfolding steps, then some rewriting, and finally a folding step. These atomic transformation rules constitute a correct and complete set for exploring the search space, however they lead to very tedious synthesis due to the no existence of a guiding plan, except for the objective of introducing recursion. The “eureka” about when and how to define a new predicate is difficult to find automatically. It is hard to decide when to stop unfolding and also there is a need for detecting symmetric transformations to avoid infinite synthesis. 4 Assertion Contexts As we said in Sect. 1, an expressive assertion is written in the language of a particular first order theory called assertion context. In Ex. 3 we show assertion context Afrom which subset’s post-condition in Ex. 1 has been written. The Herbrand universe of Ais formed out of the constants 0, [ ] and function symbols sand [ |]. Every assertion in A(idnat and member) is formalized by means of a relation symbol, a signature and a finite set of first order axioms. The Herbrand base of Ais the set of all ground atoms which can be formed by using relation symbols idnat and member with ground terms from the Herbrand universe of A. Example 3 (Assertion context from the specifier’s point of view). Assertion Context A Nat generated by 0:→Nat, s :Nat →Nat Set generated by []:→Set, [|]:Nat×Set →Set Assertion idnat :Nat×Nat idnat(0,0) ⇔true ∀x(idnat(s(x),0) ⇔false) ∀y(idnat(0,s(y)) ⇔false)∀x, y(idnat(s(x),s(y)) ⇔idnat(x, y)) Assertion member :Nat×Set ∀e(member(e, [])⇔false) ∀e, x, y(member(e, [x|y]) ⇔(idnat(x, e)∨member(e, y))) It is important to remark that assertion contexts must be processed by means of assertion checkers (i.e. software components) so reasonable restrictions have to be imposed on the form of axioms in order to make feasible their automatic processing. Example 4 shows Afrom the assertion checker’s point of view where some redundant information (i.e. layers and patterns) are explicitly shown. Example 4 (Assertion context from the assertion checker’s point of view). Assertion Context A Nat generated by 0:→Nat, s :Nat →Nat Set generated by []:→Set, [|]:Nat×Set →Set Assertion idnat :Nat×Nat idnat(0,0) ⇔true ∀x(idnat(s(x),0) ⇔false) ∀y(idnat(0,s(y)) ⇔false)∀x, y(idnat(s(x),s(y)) ⇔idnat(x, y)) Assertion member :Nat×Set ∀e(member(e, [])⇔false) ∀e, x, y(member(e, [x|y]) ⇔(idnat(x, e)∨member(e, y))) Layers. layer 0: idnat layer 1: member Patterns. l-patterns: idnat(0,0), idnat(0,s()), idnat(s( ),0), idnat(s(),s( )) member(,[]), member(,[|]) i-patterns: idnat(,0), idnat(,s( )), idnat(0,), idnat(s( ),) u-patterns: idnat(,), member(,) For the purpose of writing consistent contexts, the following restrictions have been imposed on assertions: 1. Every axiom is of the form ∀(a(x)⇔B(z)) with z⊆xwhere a(x)is an atom called the left-hand side (lhs) of the axiom and B(z)is a quantifierfree formula composed of literals and binary logical connectives called the right-hand side (rhs) of the axiom. 2. Every element in the Herbrand base of Aunifies with the lhs of a unique axiom. 3. Every assertion is encapsulated in a layer. If ais located at layer i,ais a symbol of level i. Every positive atom occurring in B(z)is defined on the symbol aor on a symbol of level i−1(if possible). Every negative atom occurring in B(z)is defined on a symbol of level i−1. 4. Every recursive specification is well-founded wrt a set of parameters. Theorem 1 (Ground Decidability). For every a(t)in the Herbrand base of Aeither Aa(t)or A¬a(t).(A proof of this theorem can be found in [12]). From Theorem 1, we formalize the semantics of assertion contexts. Our proposal is borrowed from previous results in the field of deductive synthesis [3], [14], [15]. Definition 5 (Consistency). A model for Ais defined in the following terms: A|=a(t)iff Aa(t)and A|=¬a(t)iff A¬a(t) for every a(t)in the Herbrand base of A. For the purpose of structuring the search space for new predicates [8], assertion contexts are enriched by means of a set of atom patterns. We classify atom patterns into three categories: lower patterns (l-patterns), intermediate pattern (i-patterns) and upper patterns (u-patterns). A lower pattern is calculated from the atom on the lhs of an axiom and a upper pattern is calculated from an atom on the rhs of an axiom. The rest of atom patterns (i.e. intermediate patterns) are calculated from upper and lower patterns via >(Sect. 2, Def.3): every intermediate pattern is lesser than any upper pattern and greater than any lower pattern. 5. Every atom occurring on the rhs of an axiom presents an intermediate atom pattern or a upper atom pattern. For the purpose of legibility, we display atom patterns by means of directed graphs where atom patterns are nodes and directed links are instances of the relation >. For instance, Fig. 1 shows the set of atom patterns in A(Ex. 4). idnat(_,_) (u-pattern) idnat(_,0) (i-pattern) idnat(_,s(_)) (i-pattern) idnat(0,_) (i-pattern) idnat(s(_),_) (i-pattern) idnat(0,0) (l-pattern) idnat(0,s(_)) (l-pattern) idnat(s(_),0) (l-pattern) idnat(s(_),s(_)) (l-pattern) member(_,_) (u-pattern) member(_,[ ]) (l-pattern) member(_,[_|_]) (l-pattern) Fig. 1. Graph-based description of the set of atom patterns in A. Once we have formalized the notion of assertion context, we can formalize the notion of expressive assertion. Roughly speaking, an expressive assertion is a (new) relation rintended to represent a quantified sub-formula of the form QyR(x, y) within a program assertion. Definition 6 (Expressive Assertion). We say that ris an expressive assertion in Aif and only if ris a new symbol not occurring Awhich is defined by means of a unique axiom of the form ∀x(r(x)⇔QyR(x, y)) where xis a set of variables to be instantiated at execution time, Qis a (existential or universal) quantifier and Ris a quantifier-free formula in the language of Awhere every atom presents an intermediate atom pattern or an upper atom pattern in A. Example 5 (Expressive assertion for ∀e(member(e, l)⇔member(e, s)) in subset’s post-condition (Ex. 1)). Assertion r:Set ×Set ∀l,s(r(l, s)⇔∀e(member(e, l)⇒member(e, s))) 5 Compilation Method This section explains how transformational synthesis can help to compile an expressive assertion ∀x(r(x)⇔QyR(x, y)). As we said in Sect. 1, our intentions are: If Q=∃, to synthesize a totally correct (definite) logic program r∃ 1of the form r∃ 1(x, y)⇐P∃(x, y) from an auxiliary specification ∀x, y(r∃ 1(x, y)⇔ R(x, y)) and if Q=∀, to synthesize a totally correct (definite) logic program r∀ 1 of the form r∀ 1(x, y)⇐P∀(x, y) from an auxiliary specification ∀x, y(r∀ 1(x, y)⇔ ¬R(x, y)). Example 6 (Auxiliary specification for r(Ex. 5)). In order to normalize the form of formulas (Def. 9), an equivalent formula ∀(r∀ 1(e, l, e, s)⇔¬(member(e, l)⇒ member(e, s))) is considered for ∀(r∀ 1(e, l, e, s)⇔(member(e, l)∧¬member(e, s))). Assertion r∀ 1:Nat×Set ×Nat×Set ∀e, l, s(r∀ 1(e, l, e, s)⇔(member(e, l)∧¬member(e, s))) A compilation is done by means of a finite sequence of meaning-preserving transformation steps. Each transformation step is composed of an expansion phase followed by a reduction phase. An expansion phase is intended to decompose a formula into a set of formulas and a reduction phase is intended to replace sub-formulas by new predicates. As we will show later, the set of new predicates (“recursive predicates”) is computable. 5.1 Expansion Phase Expansion phase decomposes a formula Finto a set of formulas by means of instantiations and unfolding steps. Our intention is to decomposed Fin a guided manner by using a particular rule called instantiation. To implement instantiations, we will use atom patterns in the following terms: if r(y) is a selected atom to be instantiated in Fand r(y)Pis a pattern which dominates a subgraph in the graph-based description of atom patterns for rthen lower patterns in such a subgraph will induce a set of substitutions for variables in r(y). Such sets of member(e,l) member(e,[ ]) (lower pattern) member(e,[x|y]) (lower pattern) Set of substitutions: {(l,[])} {(l,[x|y])} member(e,l) dominatesa subgraph Fig. 2. Set of substitutions for member(e, l). substitutions will be the basis to construct instantiations. In Fig. 2 we show an example of a set of substitutions for an atom. In Def(s). 7-9, we consider that Fis a formula of the form ∀(ri(x)⇔R(x)) with R(x) as a quantifier-free formula written in (the language of an assertion context) A. Definition 7 (i-Instantiation). We say that inst(F, i, a(y)) = {∀(ri(x)θ1⇔ R(x)θ1), ..., ∀(ri(x)θj⇔R(x)θj)}is the i-instantiation of an atom a(y)in Fif and only if 1. a(y)is an atom in R(x)of level iwhere a(y)Pdominates a subgraph of patterns with lower patterns {a(y1)P, ..., a(yj)P}. 2. {θ1, ..., θj}is the set of substitutions such that (a(y)θk)P=a(yk)P(k=1..j). 3. Every atom in R(x)θkpresents an atom pattern in A. Example 7 (Instantiation of member(e, l)in the axiom of r∀in Ex. 6). ∀(r∀ 1(e, [],e,s)⇔(member(e, [])∧¬member(e, s))) θ1={(l,[])} ∀(r∀ 1(e, [x|y],e,s)⇔(member(e, [x|y]) ∧¬member(e, s))) θ2={(l, [x|y])} Definition 8 (Unfolding Step). Let Ax =∀(a(x)⇔B(z)) be an axiom in an assertion context Aand a(y)an atom occurring in Fwith a(x)θ=a(y).We say that unf(F,a(y),Ax)is the unfolding step of a(y)in Fwrt Ax if and only if a(y)is replaced in Fby B(z)θ. Definition 9 (Normalization Rules). To avoid negations in front of formulas, we normalize them by using the following set of rewrite rules where Gand Hare quantifier-free formulas. (1) ¬false →true, (2) ¬true →false (3) ¬¬G→G, (4) ¬(G⇒H)→(G∧¬H) (5) ¬(G∧H)→(¬G∨¬H) (6) ¬(G∨H)→(¬G∧¬H) (7) ¬(G⇔H)→(¬(G⇒H)∨¬(H⇒G)) Definition 10 (i-Expansion). We say that the set of formulas exp(F,i)is the i-expansion of Fif and only if every formula in exp(F,i)is constructed by applying all i-instantiations (at least one) to Fand then all unfolding steps (at least one) to each resulting formula. After unfolding steps, it can appear negative sub-formulas (i.e. presence of negation in front of unfolded sub-formulas). To avoid negations in front of such sub-formulas, we normalize them. A new predicate is obtained by pattern instantiation (Ex. 10): lhs(pi(PP,B)) = r∀ 1(e, y, e, w) Finally, the replacement of Bby the new predicate produces the formula: ∀(r∀ 1(e, [x|y],e,[v|w]) ⇔ true ∧false ∧idnat(x, e)∧idnat(v,e)∨ member(e, y)∧false ∧¬idnat(x, e)∧idnat(v,e)) ∨ true ∧¬member(e, w)∧idnat(x, e)∧¬idnat(v,e)∨ r∀ 1(e, y, e, w)   lhs(pi(PP,B)) ∧¬idnat(x, e)∧¬idnat(v,e) We say that an i-reduction red(Fk,i,Ω ext(ri)) is complete when all possible folding steps have been applied to rew(Fk,P P). We say that a reduction phase has been completed for Fif and only if a complete i-reduction has been applied to every formula in exp(F,i). Theorem 4 (Reduction Preserves Correctness). Let ∀(ri(x)⇔Rred(x)) be the i-reduction of an expanded formula ∀(ri(x)⇔Rexp(x)) wrt Ωext(ri).For every ground atom ri(x)φ, A|=Rred(x)φ⇔Rexp(x)φ (A proof of this theorem can be found in [12]). 5.5 Compilation as an Incremental and Terminating Process The compilation of an axiom is completed by a finite sequence of meaningpreserving transformation steps. Each transformation step is composed of an expansion phase followed by a (complete) reduction phase. Table 2 shows r∀ 1 (Ex. 6) after a transformation step. Theorem 5 (Forms of Compiled Axioms). After a transformation step, every resulting formula presents one of the following forms. (A proof of this theorem can be found in [12]): 1. ∀(ri(x)⇔rj(x)) where rj(x)Pis equal to the lhs of some element in Ωext(ri). 2. ∀(ri(x)⇔rj(x)∧Gj(x)) where rj(x)Pis equal to the lhs of some element in Ωext(ri)and Gj(x)a conjunctive formula of literals defined on atoms whose patterns are included in A. Each transformation step represents an increment in the overall compilation process. Due to Theorem 5, each successive increment compiles either an axiom for rj(e.g. ∀(r∀ 3(e, y)⇔(member(e, y)∧false))) or an axiom for a new assertion from a literal in Gj(x) (e.g. ∀(r∀ 10(x, e)⇔¬idnat(x, e))). Theorem 6 (Termination). The compilation of an expressive assertion is completed in a finite amount of increments. (A proof of this theorem can be found in [12]). For instance, the compilation of r∀ 1(Ex. 6) has been completed by means of 11 increments (r∀ 1,...,r∀ 11). Table 2. Compilation results after one transformation step for r1 ∀ in Ex. 6. (1) ∀(r∀ 1(e, [],e,[])⇔r∀ 5) (2) ∀(r∀ 1(e, [],e,[v|w]) ⇔(r∀ 6∧idnat(v,e)∨ r∀ 2(e, w)∧¬idnat(v,e))) (3) ∀(r∀ 1(e, [x|y],e,[])⇔(r∀ 9∧idnat(x, e)∨ r∀ 5(e, y)∧¬idnat(x, e))) (4) ∀(r∀ 1(e, [x|y],e,[v|w]) ⇔(r∀ 7∧idnat(x, e)∧idnat(v,e)∨ r∀ 3(e, y)∧¬idnat(x, e)∧idnat(v, e)∨ r∀ 4(e, w)∧idnat(x, e)∧¬idnat(v,e)∨ r∀ 1(e, y, e, w)∧¬idnat(x, e)∧¬idnat(v,e))) 6 Executing Expressive Assertions from Synthesized Logic Programs Once a compilation process has been completed, a finite set of new assertions have been produced (Theorem 6). The form of their axioms (i.e. universal closure, mutually-exclusive disjunctions of conjunctions, absence of negated atoms and stratification [17]) allow to define a simple translation method from compiled assertions to definite logic programs. Definition 17 (Translation Method). For every resulting axiom Ax from a compilation: 1. If Ax is of the form ∀(r⇔P)where Pis a propositional formula formed out from constants true and false, two situations are possible: a) If the evaluation of Pis equal to false then Ax is translated to an empty clause. b) If the evaluation of Pis equal to true then Ax is translated to a clause of the form r⇐ 2. If Ax is of the form ∀(r(x)⇔k(r1(x)∧... ∧rn(x)) then it is translated to a set of kclauses of the form r(x)⇐r1(x), ..., rn(x). Every clause, which includes an atom occurrence rwith axiom of the form ∀(r⇔P)and Pequal to false, is deleted. Example 12 (Synthesized logic program for r∀ 1(Ex. 6)). r∀ 1(e, [],e,[v|w]) ⇐r∀ 2(e, w),r ∀ 10(v,e) r∀ 1(e, [x|y],e,[])⇐r∀ 11(x, e) r∀ 1(e, [x|y],e,[])⇐r∀ 5(e, y),r ∀ 10(x, e) r∀ 1(e, [x|y],e,[v|w]) ⇐r∀ 3(e, y),r ∀ 10(x, e),r∀ 11(v,e) r∀ 1(e, [x|y],e,[v|w]) ⇐r∀ 4(e, w),r ∀ 11(x, e),r∀ 10(v,e) r∀ 1(e, [x|y],e,[v|w]) ⇐r∀ 1(e, y, e, w),r ∀ 10(x, e),r∀ 10(v,e) r∀ 2(e, [x|y]) ⇐r∀ 2(e, y),r ∀ 10(x, e) r∀ 3(e, [x|y]) ⇐r∀ 3(e, y),r ∀ 10(x, e) r∀ 4(e, [])⇐r∀ 9 r∀ 4(e, [v|w]) ⇐r∀ 4(e, w),r ∀ 10(v,e) r∀ 5(e, [v|w]) ⇐r∀ 11(v,e) r∀ 5(e, [v|w]) ⇐r∀ 5(e, w),r ∀ 10(v,e) r∀ 9⇐ r∀ 10(0,s(y)) ⇐ r∀ 10(s(x),0) ⇐ r∀ 10(s(x),s(y)) ⇐r∀ 10(x, y) r∀ 11(0,0) ⇐ r∀ 11(s(x),s(y)) ⇐r∀ 11(x, y) For the purpose of verifying that synthesized logic programs are totally correct wrt goals ⇐rQ 1(t, y), a set of execution modes can be calculated for each synthesized predicate. An execution mode is formed by replacing each parameter in a signature by a mark ↓to refer to ‘a ground term as input parameter’ or ↑to refer to ‘an existentially quantified variable as output parameter’. For instance, a logic program such as the one shown in Ex. 2 is a totally correct program for idnat (Ex. 3) wrt goals ⇐idnat∀ 1(t, y) (i.e. idnat(↓,↑)), ⇐idnat∀ 1(x, t) (i.e. idnat(↑,↓)) and ⇐idnat∀ 1(t1,t 2) (i.e. idnat(↓,↓)) where t, t1,t 2are ground Nat-terms. Static analysis techniques can be used to calculate and/or verify sets of execution modes for a logic program [1], [6]. Table 3 shows the set of execution modes calculated for the synthesized program in Ex. 12. Thus, if a synthesized logic program ∀x, y(rQ 1(x, y)⇐P(x, y)) for an expressive assertion ∀x(r(x)⇔QyR(x, y)) presents rQ 1(↓,↑) as one of its execution modes then rQ 1 can be used to execute ground instances of r. For instance, such a condition holds for r∀ 1(Table 3), hence, the synthesized logic program in Ex. 12 can be used to execute ground instances of rin Ex. 5. Table 3. Execution modes for the synthesized program in Ex. 12. r∀ 11(↓,↓)r∀ 11(↑,↓)r∀ 11(↓,↑) r∀ 10(↓,↓)r∀ 10(↑,↓)r∀ 10(↓,↑) r∀ 5(↓,↓)r∀ 5(↑,↓) r∀ 4(↓,↓)r∀ 4(↑,↓) r∀ 3(↓,↓)r∀ 3(↑,↓) r∀ 2(↓,↓)r∀ 2(↑,↓) r∀ 1(↓,↓,↓,↓)r∀ 1(↑,↓,↑,↓) How can assertion checkers evaluate ground atoms r(t)from goals ⇐rQ 1(t, y) in a refutation system such as Prolog? The execution of ⇐rQ 1(t, y) in a Prolog system will compute a set of substitutions {θ1, ..., θj}for y, thus: –For Q=∃: 1. If {θ1, ..., θj}=∅then A¬∃y(r∃ 1(t, y)) (by logical consequence), A ¬∃y(R(t, y)) (by total correctness of r∃ 1), A¬r(t) (by equivalence) 2. If {θ1, ..., θj} =∅then, by a similar reasoning, A∃y(r∃ 1(t, y)), A ∃y(R(t, y)), Ar(t). –For Q=∀: 1. If {θ1, ..., θj}=∅then A¬∃y(r∀ 1(t, y)) (by logical consequence), A¬∃y(¬R(t, y)) (by total correctness of r∀ 1),A∀y(R(t, y)) (by equivalence), Ar(t) (by equivalence). 2. If {θ1, ..., θj} =∅then, by a similar reasoning, A∃y(r∀ 1(t, y)), A ∃y(¬R(t, y)),A¬∀y(R(t, y)), A¬r(t). 7 Conclusions and Future Work In this paper, we have formalized a class of assertions we call expressive assertions in the sense that they describe recursive models which are no directly translatable into executable forms. Due to this fact, current assertion checkers are not able to execute expressive assertions. The existence of mature studies in the field of transformational synthesis constitutes an important aid to overcome the problem. Recurrent problems in transformational synthesis have been revisited, for instance, the “eureka problem” (i.e. non-automatic steps about when and how to define recursive predicates). In order to overcome the problem, we restrict our attention to a particular class of first-order theories we call assertion contexts. This sort of theories is interesting because it presents a balance between expressiveness for writing assertions and existence of effective methods for compiling and executing them via synthesized (definite) logic programs. Finally, we consider that our work can also be used to construct assertion contexts in an incremental manner. In fact, assertions contexts can be extended with expressive assertions in a conservative way without losing execution capabilities. For instance, A∪r∪r∀ 1is more expressive than Awhile preserving consistency and execution capabilities (i.e. r∀ 1can be used to execute ground atoms of r). This issue is essential from a practical view point in order to reach expressive assertion languages. We plan to study it as future work. References 1. Arts, T., Zantema, H.: Termination of Logic Programs Using Semantic Unification. LOPSTR’95. Springer-Verlag, (1996) 219–233. 2. Barnes, J.: High Integrity Ada: The SPARK Approach. Addison-Wesley, (1997). 3. Bertoni, A., Mauri G., Miglioli, P.: On the Power of Model Theory in Specifying Abstract Data Types and in capturing their Recursiveness. Fundamenta Informaticae, VI(2) (1983) 27–170. 4. Burstall, R. M., Darlington, J.: A Transformational System for Developing Recursive Programs. Journal of the ACM 24(1) (1977) 44–67. 5. Bartetzko, D., Fischer, C., M¨oller, M. Wehrheim, H.: Jass-Java with Assertions. 1st Workshop on Runtime Verification. Paris. France. ENTCS Elsevier, (1999). 6. Deville, Y.: Logic Programming. Systematic Program Development. Addison- Wesley. (1990) 7. Deville, Y., Lau, K. K.: Logic Program Synthesis. J. Logic Programming 19,20 (1994) 321–350. 8. Flener, P.: Logic Program Synthesis from Incomplete Information. Kluwer Academic Publishers, Massachusetts, (1995). 9. Flener, P.: Achievements and Prospects of Program Synthesis. LNAI 2407. Springer-Verlag, (2002) 310–346. 10. Gal´an, F. J., Ca˜nete, J. M.: Improving Constructive Synthesizers by Tabulation Techniques and Domain Ordering. In David Warren (ed.), Tabulation and Parsing Deduction, (2000) 37-49. 11. Gal´an, F. J, D´ iaz, V. J., Ca˜nete, J. M.: Towards a Rigorous and Effective Functional Contract for Components. Informatica. An International Journal of Computing and Informatics. 25(4), (2001) 527–533. 12. Gal´an, F. J., Ca˜nete, J. M.: Compiling and Executing Assertions via Synthesized Logic Programs. Tecnical Report LSI-2004-01. Dept. of Language and Computer Systems. Faculty of Computer Science, Univ. of Seville. (2004) 13. Kramer, R.: iContract-The Java Design by Contract Tool. TOOLS 26: Technology of Object-Oriented Languages and Systems. IEEE Computer Society Press, (1998). 14. Lau, K., Ornaghi, M.: On Specification Frameworks and Deductive Synthesis of Logic Programs. LOPSTR’94. LNCS 883 Springer-Verlag, (1994) 104–121. 15. Lau, K., Ornaghi, M.: Towards an Object-Oriented Methodology for Deductive Synthesis of Logic Programs. LOPSTR’95. LNCS 1048 Springer-Verlag, (1995) 152–169. 16. Leavens, G., Baker, A., Ruby, C. Preliminary Design of JML. TR 98-06u, Dept. of Computer Science, Iowa State Univ., USA (2003). 17. Lloyd, J. W.: Foundations of Logic Programming, 2nd ed. Springer-Verlag, (1987). 18. Meyer, B.: Eiffel: The Language. Prentice-Hall, (1992).