Dorel Lucanu

Vlad Rusu
email: vlad.rusu@inria.fr

Program Equivalence by Circular Reasoning

Keywords: Program Equivalence, Circular Reasoning, K framework Equivalence de programmes, Raisonnement circulaire, K framework BExp ::= Bool | IExp = IExp [strict] Ids ) ≈ SExp ; SExps ::= List{SExp, ", "} Ids ::= List{Id, ", "}

We propose a logic and a deductive system for stating and automatically proving the equivalence of programs written in deterministic languages having a rewriting-based operational semantics. The chosen equivalence is parametric in a so-called observation relation, and it says that two programs satisfying the observation relation will inevitably be, in the future, in the observation relation again. This notion of equivalence generalises several well-known equivalences, and is shown to be appropriate for deterministic programs. The deductive system is circular in nature and is proved sound and weakly complete; together, these results say that, when it terminates, our system correctly solves the given program-equivalence problem. We show that our approach is suitable for proving equivalence for terminating and non-terminating programs as well as for concrete and symbolic programs. The latter are programs in which some statements or expressions are symbolic variables. By proving the equivalence between symbolic programs, one proves the equivalence of (infinitely) many concrete programs obtained by replacing the variables by concrete statements or expressions. The approach is illustrated by proving program equivalence in two languages from different programming paradigms. The examples in the paper, as well as other examples, can be checked using an online tool.

Introduction

In this paper we propose a formal notion of program equivalence, together with a languageindependent logic for expressing this notion and a deductive system for automatically proving it. Programs can belong to any deterministic language whose semantics is specified by a set of rewrite rules. The equivalence we consider is parametric in a certain observation relation, and it requires that, for all programs satisfying the observation relation, their executions eventually lead them into satisfying the observation relation again. The proof system is circular: its conclusions can be re-used as hypotheses in a controlled way. Since the problem it tries to solve is undecidable, our proof system is not guaranteed to terminate. When it does terminate, it solves the programequivalence problem as stated, thanks to its soundness and weak completeness properties.

The proposed framework is shown suitable for terminating and nonterminating programs as well as for concrete and for symbolic programs. The latter are programs in which some expressions and/or statements are symbolic variables, which denote sets of concrete programs obtained by substituting the symbolic variables by concrete expressions and/or statements. Thus, by proving the equivalence between symbolic programs, one proves in just one shot the equivalence of (possibly, infinitely) many concrete programs.

Example 1.1 We want to translate general programs with for-loops into programs with whileloops. This amounts to translating the symbolic program in the left-hand side to the one in the right-hand side.

for I from A to B do{ S } I = A ;while I <= B do { S ; I = I + 1 } Their symbolic variables I, A, B, S can be matched by, respectively, any identifier (I), arithmetical expressions (A, B), and program statement (S). We assume that the for-loop and while-loop statements have independent semantics (i.e., the for instruction is not desugared into to a while instruction) and the for loop does not modify the counter I, nor any program variables occurring in A, B (note that program variables are identifiers). If we prove the equivalence between these two symbolic programs then we also prove that every concrete instance of the for-loop is equivalent to its translation to the corresponding while-loop.

Example 1. [START_REF] Arusoaie | A Generic Framework for Symbolic Execution[END_REF] The second example illustrates the equivalence of non-terminating corecursive programs. Such programs are similar to recursive programs, but their terminating condition is missing, and therefore they describe non-terminating computations. Here we consider corecursive programs over infinite sequences of integers (also called streams). Such a program is expressed using a set of equations; for each equation, the left-hand side is the name of a function being defined, possibly with parameters, and the right-hand side is the function's body. Let us consider the corecursive program consisting of the following equations: where x ranges over integers and xs over streams. Obviously, the complete evaluation of zero produces the infinite sequence 0 : 0 : 0 : . . ., and the evaluation of one produces the infinite sequence 1 : 1 : 1 : . . ., blink produces the infinite sequence 0 : 1 : 0 : 1 : . . ., and zip( xs, ys ) produces a stream that alternates the elements of the two streams given to it as parameters. The function hd( xs ) returns the first element of the stream xs (this is the only function in the languge that does not produce a stream), and tl( xs ) returns the stream obtained from xs after removing the first element. A well-known equivalence over streams is that of blink and zip(zero,one) and many proofs of it can be found in the literature. We use this example to show that our notion of equivalence is general enough for being applicable to terminating programs as well as to non-terminating ones. The example also serves to illustrate the language-genericity of our approach.

Hereafter we often refer to symbolic programs just as "programs". A typical use of our framework consists in:

1. formally defining a programming language L, whose concrete programs are ground terms over a certain signature defining the language's syntax, and whose symbolic programs are terms with variables over that signature. The operational semantics of L is assumed given as a conditional term-rewriting system;

2. automatically constructing a new language definition L × L, whose programs are pairs of programs of L1 ;

3. applying our deductive system to programs in L × L.

Running the deductive system amounts essentially to symbolically executing the semantics of L × L, which consists in applying the rewrite rules in the semantics with unification instead of matching; details are given in the paper. This may lead to one of the following outcomes:

• termination with success, in which case the programs given as input to the deductive system are equivalent, due to the deductive system's soundness;

• termination with failure, in which case the programs given as input to the deductive system are not equivalent, due to the system's weak completeness;

• non-termination, in which case nothing can be concluded about equivalence.

Non-termination is inherent in any sound automatic system for proving program equivalence, because the equivalence problem is undecidable. We show, however, that our system terminates when the programs given to it as inputs terminate, and also when they do not terminate but behave in a certain regular way (by infinitely repeating so-called observationally equivalent configurations).

Contributions A language-independent logic and a proof system suitable for stating and proving the equivalence of concrete and of symbolic programs as well as of terminating and non-terminating ones. Programs can be written in any deterministic language that has a formal operational semantics based on term rewriting. We prove the soundness and weak completeness of the proof system, which ensure that the system correctly solves the program equivalence problem as stated. The approach is illustrated on two different languages. The examples in the paper, as well as and other examples, can be tried using an online tool, currently available at http://fmse.info.uaic.ro/tools/K/?tree=examples/prog-equiv/README. With respect to the conference paper [START_REF] Lucanu | Program Equivalence by Circular Reasoning[END_REF]: the equivalence relation is reformulated in terms of a Linear Temporal Logic (LTL) formula, and the soundness/weak completeness proofs are simpler, thanks to an encoding of executions of our proof system as the building of proofs for the LTL formulas in question. The genericity of the approach is illustrated by considering programs in two different programming paradigms.

We also generalise (for the needs of the program-equivalence approach) a generic symbolic execution technique introduced in [START_REF] Arusoaie | A Generic Framework for Symbolic Execution[END_REF]: by executing semantical rules with unification instead of matching we also allow, e.g., the symbolic execution of symbolic statements in addition to the symbolic data considered in [START_REF] Arusoaie | A Generic Framework for Symbolic Execution[END_REF].

Related Work An exhaustive bibliography on the program-equivalence problem is outside the scope of this paper, as this problem is even older than the program-verification problem. Among the recent works perhaps the closest to ours is [START_REF] Kundu | Proving optimizations correct using parameterized program equivalence[END_REF]. They also deal with the equivalence of parameterised programs (symbolic, in our terminology) and define equivalence in terms of bisimulation. Their approach is, however, very different from ours. One major difference lies in the models of programs: [START_REF] Kundu | Proving optimizations correct using parameterized program equivalence[END_REF] use CFGs (control flow graphs) of programs, while we use the operational semantics of languages. CFGs are more restricted, e.g., they are not well adapted to recursive or object-oriented programs, whereas operational semantics do not have these limitations. Of course, our advantage will only become apparent when we actually apply our approach to such programs.

Other closely related recent works are [START_REF] Godlin | Inference rules for proving the equivalence of recursive procedures[END_REF][START_REF] Godlin | Regression verification: proving the equivalence of similar programs[END_REF][START_REF] Chaki | Regression verification for multi-threaded programs[END_REF]. The first one targets programs that include recursive procedures, the second one exploits similarities between single-threaded programs in order to prove their equivalence, and the third one extends the latter to multi-threaded programs. They use operational semantics (of a specific language, which focuses on recursive procedure definition) and proof systems, and formally prove their proof system's soundness. In [START_REF] Godlin | Inference rules for proving the equivalence of recursive procedures[END_REF] they make a useful classification of equivalence relations used in program-equivalence research, and use these relations in their work.

However, all the relations classified in [START_REF] Godlin | Inference rules for proving the equivalence of recursive procedures[END_REF] are of an input/output nature: for given (sequences of) inputs, programs generate equal (sequences of) outputs and/or do not terminate. Such relations are well adapted for concrete programs with inputs and outputs, but not to symbolic programs with symbolic statements, for which a clear input-output relation may not exist. Indeed, symbolic statements may denote arbitrary concrete statements -including ones that do not perform input/output -actually, when symbolic programs are concerned, one cannot even rely on the existence of inputs and outputs. One may rely, however, on the observations of the effects of symbolic statements on the program's environment (e.g., values of variables). Our notion of equivalence (parameterised by a certain observation relation) allows this, both for finitely and for infinitely many repeated observations. Moreover, we also show that some of the relations from [START_REF] Godlin | Inference rules for proving the equivalence of recursive procedures[END_REF] can be encoded in our relation by adding information to the program environment.

Many works on program equivalence arise from the verification of compilation in a broad sense. At one end there is full compiler verification [START_REF] Leroy | Formal verification of a realistic compiler[END_REF], and at the other end, the so-called translation validation, i.e., the individual verification of each compilation [START_REF] Necula | Translation validation for an optimizing compiler[END_REF] (we only cite two of the most relevant recent works). As also observed by [START_REF] Kundu | Proving optimizations correct using parameterized program equivalence[END_REF], symbolic program verification can also be used for certain compilers, in which one proves the equivalence of each basic instruction pattern from the source language with its translation in the target language. The application of this observation to the verification of a compiler (from another project we are involved in) is ongoing and will be presented in another paper.

Several other works have targeted specific classes of languages: functional [START_REF] Pitts | Operational semantics and program equivalence[END_REF], microcode [START_REF] Arons | Formal verification of backward compatibility of microcode[END_REF], CLP [START_REF] Craciunescu | Proving the equivalence of CLP programs[END_REF]. In order to be less language-specific some works advocate the use of intermediate languages, such as [START_REF] Shuvendu | Symdiff: A language-agnostic semantic diff tool for imperative programs[END_REF], which works on the Boogie intermediate language. Only a few approaches, among which [START_REF] Leroy | Formal verification of a realistic compiler[END_REF][START_REF] Arons | Formal verification of backward compatibility of microcode[END_REF], deal with real-life language and industrial-size programs in those languages. This is in contrast to the equivalence checking of hardware circuits, which has entered mainstream industrial practice (see, e.g., [START_REF] Somenzi | Electronic Design Automation For Integrated Circuits Handbook[END_REF] for a survey).

Our proof system is inspired by that of circular coinduction [START_REF] Roşu | Circular coinduction -a proof theoretical foundation[END_REF], which allows one to prove equalities of data structures such as infinite streams and regular expressions. A notable difference between the present approach and [START_REF] Roşu | Circular coinduction -a proof theoretical foundation[END_REF] is that our specifications are essentially rewrite systems (meant to define the semantics of programming languages), whereas those of [START_REF] Roşu | Circular coinduction -a proof theoretical foundation[END_REF] are behavioural equational theories, a special class of equational specifications with visible and hidden sorts.

Symbolic linear temporal-logic model checking in term-rewriting systems, which we here use for proving program equivalence, was earlier studied in [START_REF] Escobar | Symbolic model checking of infinite-state systems using narrowing[END_REF]. There are differences in expressiveness: we only use certain specific LTL formulas for encoding equivalence, whereas [START_REF] Escobar | Symbolic model checking of infinite-state systems using narrowing[END_REF] handle full LTL; on the other hand, they consider unconditional term-rewriting systems only, whereas we also consider conditional term-rewriting systems. For our approach, which is based on programming-language semantics, having conditional rewriting systems is essential since unconditional rules are not expressive enough to express nontrivial languages semantics. There are also differences in the underlying deduction mechanisms: [START_REF] Escobar | Symbolic model checking of infinite-state systems using narrowing[END_REF] rely on powerful unificationmodulo-theories algorithms, while our unification algorithm delegates deduction to satisfiability modulo theory (SMT) solvers.

Organisation. After this introduction, Section 2.1 presents our running examples: imp, a simple imperative language, and stream, a corecursive language for handling streams of integers. Both languages are defined in K [START_REF] Roşu | An Overview of the K Semantic Framework[END_REF], a formal framework for defining operational semantics of programming languages. Our approach is, however, independent of the K framework and the imp language; hence, we present a general, abstract mechanism for language definitions in Section 3, and show how K definitions are instances of that mechanism. In Section 4 we define a unification operation and prove some properties about it, which are used in Section 5 where we present a generic symbolic execution approach for languages defined in the proposed mechanism. We formally relate symbolic execution to concrete execution, which we use later in the paper for proving the correctness properties (soundness and weak completeness) of our proof system.

In Section 6 we recap linear-temporal logic (LTL). This is then used in Section 7, which contains our proposed definition for program equivalence as the satisfiaction of certain LTL formulas over an execution of the transition system generated by (concretely) executing a pair of programs. The formula says that the programs will repeatedly satisfy a certain observation relation; this relation is a parameter of the approach. The syntax and semantics of a logic capturing the chosen equivalence are defined.

The proof system for proving equivalence formulas is presented in Section 8, together with its soundness and weak completeness. The properties say that, when it terminates, the proof system correctly answers to the question of whether its input (which is a set of formulas of program-equivalence logic) denotes equivalent programs. Their proofs are based on building proof witnesses for LTL formulas expressing equivalence. The witnesses are obtained by symbolically executing the pair of programs under investigation.

In Section 9 we report on a prototype implementation of the proof system in the K framework. This allows one to stay within the K environment when proving program equivalence for languages also defined in K. Finally, the conclusion and future work are presented in Section 10.

Two Examples of Programming Languages and their Semantics in K

We use two different languages as running examples: imp, a simple imperative language, and stream, a language for manipulating integer streams. We present their formal definitions in the K framework [START_REF] Roşu | An Overview of the K Semantic Framework[END_REF], a formal environment for defining programming languages, type systems, and analysis tools. The main ingredients of a K definition are computations, configuration, and rules.

Computations are sequences of elementary computational tasks, which consist of e.g. adding two numbers, or transforming the program being executed. A configuration is a nested structure of cells that include all the data structures required for executing a program. The rules describe how the configurations are modified when the computational tasks are performed. For details on the theoretical background of K readers can consult [START_REF] Roşu | An Overview of the K Semantic Framework[END_REF].

K language definitions can be executed and analysed using tools from the K environment. Examples of language definitions and related analysis tools can be found on the web page http: //kframework.org.

imp -A Simple Imperative Language

The first language we are using as running example is imp, a simple imperative language intensively used in research papers. A full K definition of it can be found in [START_REF] Roşu | An Overview of the K Semantic Framework[END_REF]. The syntax of imp is described in Figure 1 and is mostly self-explained. The attribute (given as an annotation) strict from the syntax means the arguments of the annotated expression/statement are evaluated before the expression/statement itself is evaluated/executed. If the attribute has as arguments a list of natural numbers, then only the arguments in positions specified by the list are evaluated before the expression/statement. The strict attribute is actually syntactic sugar for a set of K rules, briefly presented later in the section. The configuration of an imp program consists of code to be executed and an enviroment mapping identifiers to integers. In K, this is written as a nested structure of cells: here, a top cell cfg, having a cell k containing code and a cell env (see Figure 3). The sort Code2 contains statements and arithmetic and Boolean expressions. The empty code is denoted by •, and code sequencing is denoted by . Note that this is different from the sequencing operation ; of IMP.

The cell k includes the code to be executed, represented as a list of computation tasks C 1 C 2 . . ., meaning that first C 1 will be executed, then C 2 , etc. Computation tasks are typically the evaluation of statements and elementary expressions. An example of sequence of computations is given Figure 3b); this sequence is obtained by applying the heating rules generated by the strict attribute for the statement if and the operator <. The heating/cooling rules are explained latter. The cell env is an environment that binds the program variables to values; such a binding is written as a multiset of bindings of the form, e.g., x → 3.

The semantics of imp is given by a set of rules (see Figure 2) that say how the configuration evolves when the first computation task (statement or instruction) from the k cell is executed. The dots in a cell mean that the rest of the cell remains unchanged. Except for the conjunction, negation, and if statement, the semantics of each operator and statement is described by exactly one rule.

In Figure 2, the operations lookup : Map × Id → Int and update : Map × Id × Int → Map are part of the domain of maps and have the usual meanings: lookup returns the value of an identifier in a map, and update modifies the map by adding (or, if it exists, by updating) the binding of an identifier to a value. In addition to the rules in Figure 2 there are rules induced by the strictness of some statements. For example, the if statement is strict only in the first argument, meaning that this argument is evaluated before the if statement. This amounts to the following heating/cooling rules (automatically generated by K):

Code ::= Id | Int | Bool | AExp | BExp | Stmt | • | Code Code Figure 1: K Syntax of IMP I 1 + I 2 ••• k ••• cfg ⇒ I 1 + Int I 2 ••• k ••• cfg I 1 * I 2 ••• k ••• cfg ⇒ I 1 * Int I 2 ••• k ••• cfg I 1 / I 2 ••• k ••• cfg ∧ I 2 = 0 ⇒ I 1 / Int I 2 ••• k ••• cfg I 1 <= I 2 ••• k ••• cfg ⇒ I 1 ≤ Int I 2 ••• k ••• cfg true and B ••• k ••• cfg ⇒ B ••• k ••• cfg false and B ••• k ••• cfg ⇒ false ••• k ••• cfg not true ••• k ••• cfg ⇒ false ••• k ••• cfg not false ••• k ••• cfg ⇒ true ••• k ••• cfg skip ••• k ••• cfg ⇒ ••• k ••• cfg S 1 ; S 2 ••• k ••• cfg ⇒ S 1 S 2 ••• k ••• cfg { S } ••• k ••• cfg ⇒ S ••• k ••• cfg if true then S 1 else S 2 ••• k ••• cfg ⇒ S 1 ••• k ••• cfg if false then S 1 else S 2 ••• k ••• cfg ⇒ S 2 ••• k ••• cfg while B do S ••• k ••• cfg ⇒ if B then{ S ;while B do S }else skip ••• k ••• cfg for X from I 1 to I 2 do S ••• k ••• cfg ⇒ X = I 1 ;if X <= I 2 then{ S ;for X from I 1 + Int 1 to I 2 do S } else skip ••• k ••• cfg X ••• k Env env ••• cfg ⇒ lookup(Env , X ) ••• k Env env ••• cfg X = I ••• k Env env ••• cfg ⇒ ••• k update(Env , X , I ) env ••• cfg
if BE then S 1 else S 2 ••• k ••• cfg ⇒ BE if then S 1 else S 2 ••• k ••• cfg B if then S 1 else S 2 ••• k ••• cfg ⇒ if B then S 1 else S 2 ••• k ••• cfg
where BE ranges over BExp\{false, true}, B ranges over {false, true}, and is a special variable destined to receive the value of BE once it is computed. Finally, the following rules, related to the construction of terms of sort Code, complete de K definition of imp: for all C, C 1 , C 2 , C 3 : Code:

• C k ••• cfg ⇒ C k ••• cfg , and (C 1 C 2 ) C 3 k ••• cfg ⇒ C 1 (C 2 C 3 ) k ••• cfg .
The first one says that the empty sequence • is a left-neutral element, and the second one says that is right-associative.

stream -a Simple Language for Corecursive Programs

Corecursive programs differ from recursive ones by the fact that their termination condition is missing. Besides functional languages, which typically use corecursion for handling infinite data structures, several other languages have been extended to support such features (see, e.g., [START_REF] Simon | Co-logic programming: Extending logic programming with coinduction[END_REF] for an extension of Prolog, and [START_REF] Ancona | Corecursive featherweight java[END_REF] for an extension of Java). An example of a corecursive program was given in Section 1. Here we present a simple language for writing such programs over integer streams (= infinite sequence of integers). The standard semantics for corecursive functions is based on lazy evaluation, which delays the evaluation of expressions until their value is needed. For infinite expressions this evaluation is always partial, in the sense that only a finite part of the infinite expression is evaluated, e.g., a finite prefix of an infinite stream. Therefore, we say that a stream expression is a result value if it is of the form i : SE , where the integer i is the first element of the stream and SE is the rest of the stream expression. Beside the constructor _:_, two functions, often called destructors, are essential in handling streams: hd( xs ), which returns the first element of the stream, and tl( xs ), which returns the stream obtained after the first element is removed.

The syntax of the stream language is given in Figure 4. There are three expression kinds: BEXp -for boolean expressions, IEXp -integer expressions, and SExp -stream expressions. The operator X B Y is the conditional operator if B then X else Y written in a Hoare-like syntax, which is more compact. There are two kinds of statements (specifications SSpec): integer function specifications, written as f := . . . or f (. . .) := . . . (these are usual, recursive functions), and stream specifications, written as s ≈ . . . or s(. . .) ≈ . . . (these are corecursive functions)

A stream program is a sequence of function specifications, followed by an expression to be evaluated. The K configuration for stream programs is represented in Figure 5. As the snapshot suggests, the cell specs stores definitions of recursive and corecursive functions. The right-hand side of a function definition is a λ-expression, defined as follows: The cell out includes results of evaluations, which can be integers or stream result values, depending on the type of the expression to be evaluated. This cell is essential for the stream equivalence definition since it defines their observational relation. Note that the evaluation of stream expressions is an nonterminating process and the out cell includes only finite approximations of streams.

The K semantics of stream is given in Figure 6. The rules giving semantics for the boolean/integer operators that are similar to those from the imp definition and are omitted. The semantics of a function call expression consists of replacing the expression with the function body, where the formal parameters are replaced by the actual arguments (if any). The other rules are self-explained.

Example 2.1 We illustrate the semantics of stream on the following example. Assume that the current configuration is tl(one) k one → λ(). 1:one specs [] out cfg . In order to evaluate the expression tl(one), the above configuration is heated to one tl( ) k one → λ(). 1:one specs [] out cfg Now, the rule evaluating stream functions without parameters (the ninth one in Figure 6) is applied and generates the term 1:one tl( ) k one → λ(). 1:one specs [] out cfg . The expression 1:one is a result value and the corresponding cooling rule is applied, producing

tl(1:one) k one → λ(). 1:one specs [] out cfg
Applying the rule for tl and then the rule for function calls we obtain

1:one k one → λ(). 1:one specs [] out cfg
Since the content of the k cell consists only of 1:one, the rule writing in the out cell (the first one in Figure 6) can be applied the following configuration is obtained:

one k one → λ(). 1:one specs []:1 out cfg
This sequence of rules can be repeated arbitrarily (but finitely) many times, and they generate arbitrarily larger (but finite) approximations of the infinite stream one in the out cell.

I : SE k OE out ••• cfg ⇒ ⇒ ⇒ SE k OE : I out ••• cfg I k OE out ••• cfg ⇒ ⇒ ⇒ k OE : I out ••• cfg I 1 = I 2 ••• k ••• cfg ∧ ∧ ∧ I 1 = Int I 2 ⇒ ⇒ ⇒ true ••• k ••• cfg I 1 = I 2 ••• k ••• cfg ∧ ∧ ∧ I 1 = Int I 2 ⇒ ⇒ ⇒ false ••• k ••• cfg hd( I : _ ) ••• k ••• cfg ⇒ ⇒ ⇒ I ••• k ••• cfg IE 1 true IE 2 ••• k ••• cfg ⇒ ⇒ ⇒ IE 1 ••• k ••• cfg IE 1 f alse IE 2 ••• k ••• cfg ⇒ ⇒ ⇒ IE 2 ••• k ••• cfg tl( _ : SE ) ••• k ••• cfg ⇒ ⇒ ⇒ SE ••• k ••• cfg F ••• k ••• F → λ().SE ••• specs ••• cfg ⇒ ⇒ ⇒ SE ••• k ••• F → λ().SE ••• specs ••• cfg F (Vs) ••• k ••• F → λ(Xs).SE ••• specs ••• cfg ⇒ ⇒ ⇒ SE [Vs/Xs] ••• k ••• F → λ(Xs).SE ••• specs ••• cfg
where the operation [_/_] denotes syntactical substitution.

Language Definitions

Our program-equivalence approach is independent of the formal framework used for defining languages as well as from the languages being defined. We thus propose a general notion of language definition and illustrate it later in the section on the K definition of imp. We assume the reader is familiar with the basics of algebraic specification and rewriting. A language L is defined by: 1. A many-sorted algebraic signature Σ, which includes at least a sort Cfg for configurations and a subsignature Σ Bool for Booleans with their usual constants and operations. Σ may also include other subsignatures for other data sorts, depending on the language L (e.g., integers, identifiers, lists, maps,. . . ). Let Σ Data denote the subsignature of Σ consisting of all data sorts and their operations. We assume that the sort Cfg and the syntax of L are not data, i.e., they are defined in Σ \ Σ Data , and that terms of sort Cfg have subterms denoting statements (which are programs in the syntax of L) remaining to be executed. Let T Σ denote the Σ-algebra of ground terms and T Σ,s denote the set of ground terms of sort s. Given a sort-wise infinite set of variables Var , let T Σ (Var ) denote the free Σalgebra of terms with variables, T Σ,s (Var ) denote the set of terms of sort s with variables, and var (t) denote the set of variables occurring in the term t. For terms t 1 , . . . , t n we let

var (t 1 , . . . , t n ) var (t 1 ) ∪ • • • var (t n ).
For any substitution σ : Var → T Σ (Var ) and term t ∈ T Σ (Var ) we denote by tσ the term obtained by applying the substitution σ to t. We use the diagrammatical order for the composition of substitutions, i.e., for substitutions σ and σ , the composition σσ consists in first applying σ then σ .

2. A Σ-algebra T , over which the semantics of the language is defined. T interprets the data sorts (those included in the subsignature Σ Data ) according to some Σ Data -algebra D. T interprets non-data sorts as ground terms over the signature of the form (Σ \ Σ Data ) ∪ D (1) i.e., the elements of D are added to the signature Σ \ Σ Data as constants of their respective sorts. That is, a language is parametric in the way its data are implemented; it just assumes there is such an implementation D. This is important for technical reasons (existence of a unique most general unifier, discussed below). Let T s denote the elements of T that have the sort s; the elements of T Cfg are called configurations. Any valuation ρ : We explain these concepts on the imp example. Each nonterminal from the syntax (Int, Bool,. . . ) is a sort in Σ. Each production from the syntax defines an operation in Σ; for instance, the production AExp ::= AExp + AExp defines the operation _+_ : AExp × AExp → AExp. These operations define the constructors of the result sort. For the configuration sort Cfg, the only con-

Var → T is extended to a (homonymous) Σ-algebra morphism ρ : T Σ (Var ) → T . The interpretation of a ground term t in T is denoted by T t . If b ∈ T Σ,Bool (
structor is _ k _ env cfg : Code × Map Id,Int → Cfg. The expression X = I C k Env env cfg is a term of T Cfg (Var )
, where X is a variable of sort Id, I is a variable of sort Int, C is a variable of sort Code (the rest of the computation), and Env is a variable of sort Map Id,Int (the rest of the environment). The data algebra D interprets Int as the set of integers, the operations like + Int (cf. Figure 2) as the corresponding usual operation on integers, Bool as the set of Boolean values {false, true}, the operation like ∧ Bool as the usual Boolean operations, the sort Map Id,Int as the multiset of maps X → I, where X ranges over identifiers Id and I over the integers Int. The fact that maps are modified only by the update operation ensures that each identifier is bound to at most one integer value. The other sorts, AExp, BExp, Stmt, and Code, are interpreted in the algebra T as ground terms over a modification of the form (1) of the signature Σ, in which data subterms are replaced by their interpretations in D. For instance, the term if 1 > Int 0 then skip else skip is interpreted in T as if true then skip else skip, since D interprets 1 > Int 0 as D true (= true).

The rewrite rules describe the transitions over configurations, whose formal definition is given below.

Definition 3.1 (pattern [19]) A pattern is an expression of the form π ∧ ∧ ∧ φ, where π ∈ T Σ,Cfg (Var ) is a basic pattern and φ ∈ T Σ,Bool (Var ) is a boolean term called the pattern's condition. If γ ∈ T Cfg and ρ : Var → T we write (γ, ρ) |= π ∧ ∧ ∧ φ for γ = πρ and ρ |= φ. We let π ∧ ∧ ∧ φ denote the set {γ | there exists ρ such that (γ, ρ) |= π ∧ ∧ ∧ φ}.
For any set of patterns Φ we let Φ ϕ∈Φ ϕ . A basic pattern π thus defines a set of (concrete) configurations, and the condition b gives additional constraints these configurations must satisfy. In [START_REF] Roşu | Checking reachability using matching logic[END_REF] patterns are encoded as FOL formulas, hence the conjunction notation π ∧ ∧ ∧ b. In this paper we keep the notation but separate basic patterns from constraining formulas. We often identify basic patterns π with patterns π ∧ ∧ ∧ true.

Examples of patterns are

I 1 + I 2 C k Env env cfg and I 1 / I 2 C k Env env cfg ∧ ∧ ∧ I 2 = Int 0.
An example of configuration that satisfies the second pattern is (4 / 3) skip k a → 5 env cfg . Remark 3.1 Any pattern π ∧ ∧ ∧ φ can be transformed into a "semantically equivalent" pattern π ∧ ∧ ∧ φ (i.e.., π ∧ ∧ ∧ φ = π ∧ ∧ ∧ φ ) such that π is linear and all its data subterms are variables. For this, just replace all duplicated variables and all non-variable data subterms of π by fresh variables, and add constraints to equate in φ the fresh variables to what they replaced. The transformations are presented in detail in [START_REF] Arusoaie | A Generic Approach to Symbolic Execution[END_REF].

Example 3.1 The pattern X / Y k Y → A + Int 1 env cfg ∧ ∧ ∧ A = Int -1 with X, Y
X / Y k Y → A env cfg ∧ ∧ ∧ Y = Id Y ∧ Bool A = Int A + Int 1 ∧ Bool A = Int -1
The proof system we propose in Section 8 uses as a basic block the testing of inclusions of the form ϕ ⊆ ϕ . Therefore we need criteria for such inclusions. The following lemmas define sufficient conditions. Proposition 3.1 Let π and π be two basic patterns and σ a substitution such that π σ = π, yσ = y for all y ∈ var (π ), and var (π

) ∩ var (π ∧ ∧ ∧ φ) = ∅. Then π ∧ ∧ ∧ φ = π ∧ ∧ ∧ ( σ ∧ φ) , where σ denotes the conjunction x∈var (π ) x = xσ.
Proof We prove the equality of the two sets by double inclusion.

(⊆) Let γ ∈ π ∧ ∧ ∧ φ . Then there is ρ : Var → T such that γ = πρ and ρ |= φ. Let ρ denote the valuation ρ : Var → T given by xρ = xσρ for x ∈ var (π ), and yρ = yρ for y ∈ var (π ). We have

π ρ = π σρ = πρ = γ. Since var (φ) ∩ var (π ) = ∅, it follows that ρ |= φ iff ρ |= φ. Finally, var (π ) ∩ var (π) = ∅ implies var (π ) ∩ var (σ(x)) = ∅ and hence xσρ = xσρ for x ∈ var (π ). Now, π ρ = γ that implies γ ∈ π ∧ ∧ ∧ σ ∧φ) . Since γ was chosen arbitrarily, it follows that π ∧ ∧ ∧ φ ⊆ π ∧ ∧ ∧ ( σ ∧ φ) .
(⊇) Assume that γ ∈ (π ∧ ∧ ∧ σ ∧φ) . Then there is ρ : Var → T such that γ = π ρ , and ρ |= ( σ ∧φ). From ρ |= σ we get xρ = xσρ for x ∈ var (π ), which implies γ = π ρ = π σρ = πρ. Hence γ ∈ π ∧ ∧ ∧ φ . Since γ was chosen arbitrarily, it follows that π ∧ ∧ ∧ ( σ ∧ φ) ⊆ π ∧ ∧ ∧ φ . Proposition 3.2 Let π ∧ ∧ ∧ φ and π ∧ ∧ ∧ φ be two patterns and σ a substitution such that π σ = π, yσ = y for all y ∈ var (π ), and var (π

) ∩ var (π ∧ ∧ ∧ φ) = ∅. If σ ∧ φ implies φ , then π ∧ ∧ ∧ φ ⊆ π ∧ ∧ ∧ φ . Proof Let γ ∈ π ∧ ∧ ∧ φ.
Then there is a valuation ρ such that γ = πρ and ρ |= φ. Let ρ be defined as in Proposition 3.1. Then π ρ = γ and ρ |= σ ∧ φ that implies ρ |= φ by the hypotheses. Hence γ ∈ π ∧ ∧ ∧ φ . Since γ was chosen arbitrarily, we may conclude the conclusion of the proposition.

(π ∧ ∧ ∧ φ )σ = π ∧ ∧ ∧ φ. Then π ∧ ∧ ∧ φ ⊆ π ∧ ∧ ∧ φ . Proof Let γ ∈ π ∧ ∧ ∧ φ.
Then there is a valuation ρ such that γ = πρ and ρ |= φ. Let ρ be defined by xρ = xσρ for each x in Var . It follows π ρ = π σρ = πρ = γ and similarly φ ρ = φρ that implies ρ |= φ . Since γ was chosen arbitrarily, we may conclude the conclusion of the proposition.

We are now ready to define semantical rules and the transition system that they generate. Definition 3.2 (semantical rule and transition system [START_REF] Roşu | Checking reachability using matching logic[END_REF]) A rule is a pair of patterns of the form l ∧ ∧ ∧ b ⇒ ⇒ ⇒ r (where r is the pattern r ∧ ∧ ∧ true). Any set S of rules defines a labelled transition system (T Cfg , ⇒ S ), where γ ⇒ S γ iff there are α (l ∧ ∧ ∧ b ⇒ ⇒ ⇒ r) ∈ S and ρ : Var → T such that (γ, ρ) |= l ∧ ∧ ∧ b and (γ , ρ) |= r.

Assumption 1 We assume without restriction of generality that for all rules l ∧ ∧ ∧ b ⇒ ⇒ ⇒ r ∈ S, l is linear and all its data subterms are variables. The generality is not restricted because the pattern l ∧ ∧ ∧ b in the rule l ∧ ∧ ∧ b ⇒ ⇒ ⇒ r ∈ S can always be replaced by an equivalent one (cf. Remark 3.1) with the desired properties. This transformation of rules does not modify the transition system (T Cfg , ⇒ S ).

Unification

We shall be using unification both for defining our program-equivalence proof system and for proving properties about it. In this section we define unification and prove a technical lemma used later in the paper. Definition 4.1 (Unifiers) A symbolic unifier of two terms t 1 , t 2 is any substitution σ : var (t 1 ) var (t 2 ) → T Σ (Z) for some set Z of variables such that t 1 σ = t 2 σ. A concrete unifier of terms t 1 , t 2 is any valuation ρ : var (t 1 ) var (t 2 ) → T such that t 1 ρ = t 2 ρ. A symbolic unifier σ of two terms t 1 , t 2 is a most general unifier of t 1 , t 2 with respect to concrete unification whenever, for all concrete unifiers ρ of t 1 and t 2 , there is a valuation η such that ση = ρ. We often call a symbolic unifier satisfying the above a most general unifier 3 .

We say that terms t 1 , t 2 are symbolically (resp. concretely) unifiable if they have a symbolic (resp. concrete) unifier. The next lemma gives conditions under which concretely unifiable terms are symbolically unifiable. Lemma 4.1 All linear, concretely unifiable terms t 1 , t 2 ∈ T Σ (Var ), such that all their data subterms are variables, are symbolically unifiable by a most general unifier σ t1 t2 : var (t 1 ) var (t 2 ) → T Σ (var (t 1 ) var (t 2 )).

Proof By induction on the structure of, say, t 1 . In the base case, t 1 ∈ Var , and we take σ t1 t2 (t 1 → t 2 ) Id| var (t2) , i.e., σ t1 t2 maps t 1 to t 2 , and is the identity on var (t 2 ). Obviously, σ t1 t2 is a unifier of t 1 , t 2 , since t 1 σ t1 t2 = t 2 . To show that σ t1 t2 is most general, consider any concrete unifier of t 1 , t 2 , say, ρ. Then, t 1 σ t1 t2 ρ = t 2 ρ because σ t1 t2 maps t 1 to t 2 , and t 2 ρ = t 1 ρ because ρ is a concrete unifier. Thus, t 1 σ t1 t2 ρ = t 1 ρ. Moreover, for all x ∈ var (t 2 ), xσ t1 t2 ρ = xρ since σ t1 t2 is the identity on var (t 2 ). Thus, for all y ∈ var (t 1 ) var (t 2 )(= {t 1 } var (t 2 )), yσ t1 t2 ρ = yρ, which proves the fact that σ t1 t2 is a most general unifier (by taking η = ρ in Definition 4.1 of unifiers). The fact that the codomain of σ t1 t2 is T Σ (var (t 1 ) var (t 2 )) results from its construction. In the inductive step, t 1 = f (s 1 , . . . , s n ) with f ∈ Σ\Σ Data4 n ≥ 0, and s 1 , . . . , s n ∈ T Σ (Var ). For t 2 there are two subcases:

• t 2 is a variable. Then, let σ t1 t2 (t 2 → t 1 ) Id| var (t1) , i.e., σ t1 t2 maps t 2 to t 1 , and is the identity on var (t 1 ). We prove that σ t1 t2 is a most general unifier with codomain T Σ (var (t 1 ) var (t 2 )) like in the base case.

• t 2 = g(u 1 , . . . , u m ) with g ∈ Σ, m ≥ 0, and u 1 , . . . , u m ∈ T Σ (Var ). Let ρ be a concrete unifier of t 1 , t 2 , thus, (f ρ)(s 1 ρ . . . s n ρ) = T (gρ)(u 1 ρ . . . u m ρ), where we emphasize by subscripting the equality symbol with T that the equality is that of the model T . Since T interprets non-data terms as ground terms over the modified signature (1), we have f ρ = f , which implies f = g, gρ = g, m = n, and s i ρ = u i ρ for i = 1, . . . , n. Since t 1 and t 2 are linear and all their data subterms are variables, the subterms s i and u i also have these properties. Using the induction hypothesis we build most-general-unifiers σ si ui of s i and u i , which have codomains T Σ (var (s i ) var (u i )), for i = 1, . . . , n. Let then σ t1 t2 n i=1 σ si ui . First, σ t1 t2 is a substitution of var (t 1 ) var (t 2 ) into T Σ (var (t 1 ) var (t 2 )) since var (t 1 ) = n i=1 var (s i ) and var (t 2 ) = n i=1 var (u i ). Note that these equalities hold thanks to the linearity of t 1 , t 2 . Second, σ t1 t2 is a unifier of t 1 , t 2 since all σ si ui are so. Third, we prove that σ t1 t2 is a most general unifier of t 1 , t 2 . Consider any concrete unifier ρ of t 1 and t 2 , thus, s i ρ = u i ρ for i = 1, . . . , n. From the fact that all the σ si ui are most-general-unifiers of s i and u i for i = 1, . . . , n, we obtain the existence of valuations η i such that σ si ui η i = ρ| (var (si) var (ui)) , for i = 1, . . . , n. Then, η n i=1 η i , which is also well-defined thanks to the linearity of t 1 and t 2 , has the property that σ t1 t2 η = ρ, which proves that σ t1 t2 is a most general unifier of t 1 and t 2 and concludes the proof.

Symbolic Execution

In this section we present a symbolic execution approach for languages defined using the languagedefinition framework presented in the previous section. We prove that the transition system generated by symbolic execution forward-simulates the one generated by concrete execution, and that the transition system generated by concrete execution backward-simulates the one generated by symbolic execution (restricted to satisfiable patterns). This is used later for proving correctness results for our program-equivalance deduction system.

Symbolic execution consists of applying the semantical rules over patterns using most general unifiers. This generalises the symbolic execution approach proposed in [START_REF] Arusoaie | A Generic Framework for Symbolic Execution[END_REF], where unification was encoded using matching with modified rules, and which did not allow for symbolic statements. Symbolic execution generates a symbolic transition system whose states are patterns, and whose transition relation is obtained by applying rewrite rules with the most-general unifiers whose construction is given by Lemma 4.1.

∆ S (ϕ) {ϕ | ϕ ⇒ s S ϕ }. A pattern ϕ is derivable if ∆ S (ϕ) is a nonempty set.
In the rest of the paper, for patterns ϕ π ∧ ∧ ∧ φ we let var (ϕ) var (π, φ), and for rules α l ∧ ∧ ∧ r ⇒ ⇒ ⇒ b we let var (α) var (l, b, r). Moreover, for symbolic transitions ϕ ⇒ s S ϕ we assume without restriction on generality that var (ϕ) ∩ var (α) = ∅, which can always be obtained by variable renaming. We also omit to write the subscript S in the derivatives notation whenever it is understood from the context. ). Using Lemma 4.1 we obtain their unique most-general symbolic unifier σ l π , whose codomain is T Σ (var (l) var (π)). Let then η : var (l) var (π) → T be the valuation such that σ l π η = ρ| var (l) µ| var (π) . We extend σ l π to var (ϕ, α) by letting it be the identity on var (ϕ, α) \ var (l, π), and extend η to var (ϕ, α) such that η| var (b,r)\var (l) = ρ| var (b,r)\var (l) and η| var (φ)\var (π) = µ| var (φ)\var (π) . With these extensions we have x(σ l π η) = x(ρ µ) for all x ∈ var (ϕ, α).

Let ϕ rσ l π ∧ ∧ ∧ (φ ∧ b)σ l π : we have the transition ϕ ⇒ s S ϕ by definition of the symbolic transition system. There remains to prove γ ∈ ϕ .

• on the one hand, (rσ l π )η = r(σ l π η) = r(ρ µ) = rρ = γ ; thus, (γ , η) |= rσ l π ;

• on the other hand,

((φ ∧ b)σ l π )η = φ(σ l π η) ∧ b(σ l π η) = φ(ρ µ) ∧ b(ρ µ) = φµ ∧ bρ = true since φµ = bρ = true; thus; η |= ((φ ∧ b)σ l π ).
The two above items imply (γ , η) |= rσ l π ∧ ∧ ∧ (φ ∧ b)σ l π , i.e., (γ , η) |= ϕ , which concludes the proof. • From γ = lρ using the definition of ρ we get

Corollary 5.1 For every concrete execution γ

0 ⇒ S γ 1 ⇒ S • • • ⇒ S γ n ⇒ S • • • there is a symbolic execution ϕ 0 ⇒ s S ϕ 1 ⇒ s S • • • ⇒ s S ϕ n ⇒ s S • • • such that γ i ∈ ϕ i for i = 0, 1, . . ..
γ = lρ = l(σ l π η) = (lσ l π )η = (πσ l π )η = π(σ l π η) = πρ; • From ((φ ∧ b)σ l π )η = true we obtain (φσ l π )η = φ(σ l π η) = φρ = true.
Since ϕ π ∧ ∧ ∧ φ, the last two items imply (γ, ρ) |= ϕ, which completes the proof. We call a symbolic execution feasible if all its patterns are satisfiable (a pattern ϕ is satisfiable if there is a configuration γ such that γ ∈ ϕ ).

Corollary 5.2 For every feasible symbolic execution ϕ

0 ⇒ s S ϕ 1 • • • ⇒ s S ϕ n ⇒ s S • • • there is a concrete execution γ 0 ⇒ S γ 1 ⇒ S • • • ⇒ S γ n ⇒ S • • • such that γ i ∈ ϕ i for i = 0, 1, . . ..

Linear Temporal Logic

The notion of program equivalence we propose uses Linear Temporal Logic (LTL) formulas, defined below.

A Kripke structure is a tuple (S, ⇒, P, λ, S i ) where S is a set of states, ⇒⊆ S × S is a (total) transition relation, P is a set of propositions, λ : S → 2 P is the labelling function, and S i ⊆ S is the set of initial states.

An execution e s 0 , . . . , s n , . . . is a sequence of states such that s 0 ∈ S i and s j ⇒ s j+1 for all j ∈ N. The suffix of an execution e from l ∈ N, denoted by e l , is the sequence such that e l (j) = s l+j for all j ∈ N. • e |= ¬ψ iff it is not the case that e |= ψ;

• e |= ψ 1 Uψ 2 iff there exists k > 0 such that e k |= ψ 2 and for all 0 ≤ j < k, e j |= ψ 1 .

We will be be interested in formulas of the form ♦p. Using the semantics of LTL, an execution e = s 0 , . . . , s n , . . . satisfies ♦p iff it has an infinite subsequence s i1 , . . . s im , . . . such that p ∈ λ(s ij ) for all j ∈ N.

Defining Program Equivalence

We define in this section our notion of program equivalence and a logic for stating equivalence properties.

Assumption 2 We assume without restriction of generality that the transition system (T Cfg , ⇒ S ) has no terminal states (i.e., its transition relation is total). This can always be obtained by adding to S rules of the form π ⇒ ⇒ ⇒ π for all non-derivable patterns π, which just add self-loops to terminal states of (T Cfg , ⇒ S ).

Remark 7.1 Strictly speaking, it is not programs that are the subject of equivalence, but full configurations (of which programs are just one component). Indeed, program executions depend on the rest of the configuration (e.g., initial values of the variables, . . . ). Hence, the equivalence relation is a relation on T Cfg .

We consider a given observation relation O ⊆ T Cfg × T Cfg , which shall serve as a parameter to our equivalence. Then, we say that two configurations are observationally equivalent if they are in the observation relation.

Observational equivalence should be understood as a purely local property of configuration pairs, such as, e.g., a given set of variables have the same values in both configurations. Then, our notion of program equivalence requires that starting from any two observationally equivalent configurations, by executing the programs in the configuration one will eventually encounter observationally equivalent configurations again. This expressed by the LTL formula O ∧ ♦O, which captures precisely the informal meaning given above. In order to formalise this observation, it will be convenient to consider, for a given language definition L, the language definition denoted by L 2 , whose configurations are pairs of configurations of L and whose rewrite rules are those of L, lifted at the level of configurations of L 2 ; that is, each semantical rule l ∧ ∧ ∧ b ⇒ ⇒ ⇒ r of L generates two rules of L 2 : l, X ∧ ∧ ∧ b ⇒ ⇒ ⇒ r, X and Y, l ∧ ∧ ∧ b ⇒ ⇒ ⇒ Y, r where _, _ is the configuration constructor for L 2 and X, Y are variables of sort Cfg for L that do not occur in the rest of the rule.

Let S 2 l denote the set of rules of L 2 of the form l, X ∧ ∧ ∧ b ⇒ ⇒ ⇒ r, X , and S 2 r denote the set of rules of L 2 of the form Y, l ∧ ∧ ∧ b ⇒ ⇒ ⇒ Y, r . We denote by S 2 the whole set of rules of L 2 , i.e.,

S 2 = S 2 l S 2
r . We transform the transition system of L 2 into a Kripke structure by regarding the observation relation O as a proposition and by labelling the states γ 1 , γ 2 of the transition system with O iff (γ 1 , γ 2 ) ∈ O.

By K γ1,γ2 we denote the Kripke structure thus constructed, endowed with the single initial state γ 1 , γ 2 . Definition 7.1 Two configurations γ 1 , γ 2 are equivalent, written γ 1 ∼ γ 2 , if there exists an execution e of the Kripke structure K γ1,γ2 such that e |= O ∧ ♦O.

Example 7.1 The two following configurations:

γ 1 x = 2 k x → 0 env cfg and γ 1 y = 1; y = y+1 k y → 0 env cfg
are equivalent when O is defined by requiring that x = y. Indeed, in imp 2 , starting from γ 1 , γ 2 there is an execution reaching the self-looping state k x → 2 env cfg , k y → 2 env cfg , which is in O, hence, the execution satisfies O ∧ ♦O. Note that not all executions of imp 2 starting in γ 1 , γ 2 satisfy O ∧ ♦O, for example, an execution that applies only rules form S l (imp 2 ) followed by self-looping rules violates O ∧ ♦O.

Remark 7.2

The relation O gives us quite a lot of expressiveness for capturing various (deterministic) program equivalences, such as the ones classified in [START_REF] Godlin | Inference rules for proving the equivalence of recursive procedures[END_REF]. For example, partial equivalence is: two programs are equivalent if, whenever presented with the same input, if they both terminate then they produce the same output. This can be encoded by including cells in the configuration for the input and output, and by including in O the pairs of configurations satisfying: if programs are both empty and inputs are equal then outputs are equal as well. Also, full equivalence states that two programs are equivalent if, whenever presented with the same input, they either both terminate and produce the same output, or they both do not terminate. This is captured by adding to the above relation all pairs of configurations from which there exist executions starting from both configurations of the pair, such that the programs in both configurations are forever nonempty. Finally, reactive equivalence requires that two programs, when presented with the same sequence of inputs, produce the same sequence of outputs. To encode this equivalence we include in O all configuration pairs satisfying: if the input cells are equal then the output cells are equal as well.

Remark 7.3

The chosen definition of equivalence does not work for nondeterministic programs. Indeed, assume a nondeterministic instruction | such that, for any statements S 1 , S 2 , the statement S 1 | S 2 rewrites to either S 1 or S 2 . Then, the nondeterministic program (x:= 0) | (x:= 1) is not equivalent to itself according to our definition (with O being the relation that requires equality of x in both copies of the program). Indeed, one copy of the program can perform x := 0 and self-loop there, while the other one performs x := 0 and self-loop there. For the quivalence of nondeterministic programs, the adequate notion of equivalence requires that for all executions e of one program, there exists an execution e of the other one and an interleaving of e, e satisfying O ∧ ♦O. This alternation of quantifiers induces additional difficulties for the verification.

We present in the rest of the section a logic for program equivalence. We present the logic's syntax and a notion of validity for formulas. A derivative operation for formulas is also defined.

Definition 7.2 (Syntax)

A formula is a pattern of L 2 according to Def. 3.1 applied to L 2 , i.e., an expression of the form π 1 , π 2 ∧ ∧ ∧ φ where π 1 , π 2 ∈ T Σ,Cfg (Var ) are basic patterns of L and C ∈ T Σ,Bool (Var ).

Example 7.2 Assume that the signature Σ for the language imp contains a predicate isModified : Id × Stmt → Bool, expressing the fact that the value of the given identifier is modified by the semantics of the given statement. A formula expressing the equivalence of the programs in Example 1.1 is

for I from A to B do{ S } k , M env cfg I = A ;while I <= B do{ S ; I = I + 1 } k , M env cfg ∧ ∧ ∧ ¬ Bool isModified (I, S) ∧ ¬ Bool isModified (A, S) ∧ ¬ Bool isModified (B, S)
where M a variable of sort Map. The condition says that the loop counter I is not modified in the body S, and the variables occuring in A, B are not modified by S either. The Boolean function isModified () is defined by structural induction on its arguments in the expected manner.

Recall that the set f , introduced by Definition 3.1 applied to L 2 is the set of configurations γ 1 , γ 2 of L 2 such that γ 1 , γ 2 ∈ f . Definition 7.3 (Validity) A formula ϕ is valid, written S |≡ϕ, if for all γ 1 , γ 2 ∈ ϕ , γ 1 ∼ γ 2 .

For the deductive system we shall also be needing the following definition: the derivative of a formula f is the set of formulas defined by Definition. 5.2, applied to the symbolic transition of the language L 2 . We denote it by ∆ S 2 (f ). We let ∆ l (f ) ∆ S 2 l (f ) be the left-derivative and ∆ r (f ) ∆ S 2 r (f ) be the right-derivative of f . We conclude this section by the following lemma that will be used in proofs regarding our deductive system. Lemma 7.1 For all patterns ϕ π 1 , π 2 ∧ ∧ ∧ φ of L 2 , all instances γ 1 , γ 2 ∈ ϕ , and all h ∈ {l, r}, there exists ϕ ∈ ∆ h (ϕ) and

γ 1 , γ 2 ∈ ϕ such that γ 1 , γ 2 ⇒ S 2 γ 1 , γ 2 .
Proof We prove the lemma for h = l, the other case being similar. By construction of the language L 2 , the pattern ϕ has the form π 1 , π 2 ∧ ∧ ∧ φ, where π 1 , π 2 are basic patterns of L, i.e., terms of sort Cfg in L, and φ is a term of sort Bool . Thus, π 1 ∧ ∧ ∧ φ is a pattern of L. On the other hand, there exists γ 1 such that γ 1 ⇒ S γ 1 because the transition system (T Cfg , ⇒ S ) has no terminal states (Assumption 2). From γ 1 ⇒ S γ 1 we obtain ρ : Var → T and α = (l ∧ ∧ ∧ b ⇒ ⇒ ⇒ r) ∈ S such that γ 1 = lρ, γ 1 = rρ, and bρ = true. By construction of L 2 , there is a rule l, X ∧ ∧ ∧ b ⇒ ⇒ ⇒ r, X ∈ S 2 l for X a variable of sort Cfg not ocurring in the rest of the rule, i.e., satisfying Xρ = X. By extending ρ into a valuation ρ such that Xρ = γ 2 we obtain the concrete transition γ 1 , γ 2 ⇒ S 2 γ 1 , γ 2 . Using Lemma 5.1 applied to the transition γ 1 , γ 2 ⇒ S 2 γ 1 , γ 2 and the pattern ϕ we obtain a pattern ϕ such that γ 1 , γ 2 ∈ ϕ and ϕ ⇒ s S 2 l ϕ , because the rule that is symbolically applied to obtain ϕ from ϕ is l, X ∧ ∧ ∧ b ⇒ ⇒ ⇒ r, X ∈ S 2 l . Thus, ϕ ∈ ∆ l (ϕ), which proves the lemma.

In this section we define a four-rule proof system for proving program equivalence. It is inspired from circular coinduction [START_REF] Roşu | Circular coinduction -a proof theoretical foundation[END_REF], a coinductive proof technique for infinite data structures and coalgebras of expressions [START_REF] Bonsangue | A decision procedure for bisimilarity of generalized regular expressions[END_REF]. Remember that we have fixed an observation relation O. We assume a set of formulas Ω such that Ω = O. Let also be an entailment relation satisfying S, F ϕ implies (S |≡ ϕ or there exists f ∈ F such that ϕ ⊆ f ). The set Ω and the relation are parameters of our proof system:

Definition 8.1 (Circular Proof System) [Axiom] S, F ∅ [Reduce] S, F G S, F G ∪ {ϕ} if S, F ϕ [Circularity] S, F ∪ {ϕ} G ∪ ∆ h (ϕ) h ∈ {l, r} S, F G ∪ {ϕ} if ϕ ⊆ Ω [Derive] S, F G ∪ ∆ h (ϕ) h ∈ {l, r} S, F G ∪ {ϕ} if ϕ ⊆ Ω and ∆ h (ϕ) = {ϕ}
An execution of the proof system is any sequence δ of applications of the above rule. For Γ a set of formulas (also called goals), a proof of S Γ is an execution whose last rule is [Axiom].

[Axiom] says that when an empty set of goals is reached, the proof is finished. The [Reduce] rule removes from the current set of goals G any goal that can be discharged by the entailment . The last two rules, [Circularity] and [Derive], both say that a goal ϕ is are replaced by either its left of right derivatives in the set of goals to be proved. However, in [Circularity], the goal ϕ is added as hypotheses provided that ϕ ⊆ Ω , i.e., provided that all its instances are observationally equivalent pairs of configurations. Thus, all the hypotheses f added during executions satisfy f ⊆ Ω = O. On the other hand, if ϕ ⊆ Ω then the [Derive] rule can be applied, which adds no hypotheses: a goal ϕ in the current set of goals G is just replaced by its set of left or dight-derivatives, provided that they are not ϕ itself, i.e., to ensure that [Derive] does not apply uselessly.

The soundness of our proof system is the consequence of the following lemmas. By sequent encountered by δ we mean any sequent S, F G which is obtained by applying a prefix of the sequence δ of rules. Lemma 8.1 For all sequents S, F G ∪ {ϕ} encountered by δ, for all γ 1 , γ 2 ∈ ϕ , there exists a sequent S, F G ∪ {ϕ } encountered by δ with ϕ ⊆ O, and

γ 1 , γ 2 ∈ ϕ , such that γ 1 , γ 2 ⇒ * S 2 γ 1 , γ 2 .
Proof By (strong) induction on the length of the proof δ and case analysis. Depending on first the rule of δ that is applied to the sequent S, F G ∪ {ϕ}:

• if the rule is [Reduce] then there are two subcases:

if S ϕ then S |≡ ϕ. Thus, γ 1 , γ 2 ∈ ϕ ⊆ O, and we let F = F , G = G, ϕ = ϕ, and γ 1 , γ 2 = γ 1 , γ 2 ;

if ϕ ⊆ f for some f ∈ F then ϕ ⊆ O since all hypotheses f are added (by [Circularity]) such that f ⊆ Ω = O, and we can also take F = F , G = G, ϕ = ϕ, and γ 1 , γ 2 = γ 1 , γ 2 ;

• if the rule is [Derive] or [Circularity]: using Lemma 7.1, for any γ 1 , γ 2 ∈ ϕ , there exists ϕ ∈ ∆ h (ϕ) and γ 1 , γ 2 ∈ ϕ such that γ 1 , γ 2 ⇒ S 2 γ 1 , γ 2 . Moreover, the goal ϕ is the current goal of a future rule application in δ and is the origin of a proof δ strictly shorter than δ. Using the induction hypothesis, there exists S,

F G ∪ {ϕ } and γ 1 , γ 2 ∈ ϕ ⊆ O such that γ 1 , γ 2 ⇒ * S 2 γ 1 , γ 2 . . By transitivity γ 1 , γ 2 ∈ ϕ ⇒ * S 2
γ 1 , γ 2 holds, which proves this case and concludes the proof.

The next lemma says that, for each instance of each hypothesis that has actually been used for discharging a goal during a proof, there a strict successor of it satisfying the current goal of some encountered sequent. Lemma 8.2 Let Φ denote the set of all hypotheses used for discharging a subgoal during the proof δ (i.e., using a [Reduce] rule). Then, for all sequents S, F G encountered by δ, for all f ∈ F ∩ Φ, and for all γ 1 , γ 2 ∈ f , P (f, γ 1 , γ 2 ) there exists γ 1 , γ 2 and a sequent S, F G ∪ {ϕ } encountered by δ with ϕ ⊆ O, such that γ 1 , γ 2 ∈ ϕ and

γ 1 , γ 2 ⇒ + S 2 γ 1 , γ 2 hold.
Proof We show that the lemma's statement holds initially and that it is preserved (as an invariant) by all applications of rules in our deductive system (in particular, for the rules in the proof δ). The lemma's statement is trivially true initially, when F = ∅. For the induction step, we assume that the lemma's statement holds for the current sequent S, F G ∪ {ϕ} and we show that it holds in the next sequent (if any) in δ.

• if the next rule is [Reduce] there are two subcases:

-S ϕ. The set F ∩ Φ in the next sequent is the same as in the current one, since this reduction does not use hypotheses in F . With the same instance γ 1 , γ 2 and sequent S, F G ∪ {ϕ } given by the inductive hypothesis, we establish that the lemma's statement still holds in the next sequent.

ϕ ⊆ f 0 for some f 0 ∈ F . In this case the set F ∩ Φ in the next sequent is (possibly) larger than in the current one, since this may be the first time the hypothesis f 0 is used to discharge a goal (here, ϕ). (If F ∩ Φ is the same in the next sequent as in the current one, the inductive hypothesis trivially proves, like in the previous case S ϕ, that our lemma's statement still holds in the next sequent.) Thus, there remains to consider the case where the current rule's application is the first-time use of the hypothesis f to discharge a goal (here, ϕ), in which case we have to prove P (f, γ 1 , γ 2 ) for all f ∈ F ∪ {f 0 } and γ 1 , γ 2 ∈ f . Now, P (f, γ 1 , γ 2 ) for f ∈ F and γ 1 , γ 2 ∈ f holds using the inductive hypothesis (this is proved as in the case S ϕ). There remains to prove P (f 0 , γ 1 , γ 2 ) for all γ 1 , γ 2 ∈ f 0 . For this, we note that f 0 has been added to F at an earlier proof step by [Circularity], and f 0 was replaced in the following sequent's goals by its derivatives ∆ h (f 0 ) for some h ∈ {l, r}. Using Lemma 7.1, we obtain a goal

f 0 ∈ ∆ h (f 0 ) and γ 1 , γ 2 ∈ f 0 such that γ 1 , γ 2 ⇒ S 2 γ 1 , γ 2 . Using Lemma 8.1 we obtain the instance γ 1 , γ 2 and the sequent S, F G ∪ {ϕ } such that γ 1 , γ 2 ∈ ϕ ⊆ O and γ 1 , γ 2 ⇒ * S 2 γ 1 , γ 2 . By transitivity, γ 1 , γ 2 ⇒ + S 2 γ 1 , γ 2
, which proves that P (f 0 , γ 1 , γ 2 ) holds for all γ 1 , γ 2 ∈ f 0 : the lemma's statement still holds in the next sequent.

• if the next rule is [Circularity] or [Derive]: in this case F ∩ Φ in the next sequent is the same as in the current one, since this rule does not eliminate goals using circular hypotheses (even though, in the case of [Circularity] the current set of hypotheses grows). Like in the case S ϕ we establish that the lemma's statement still holds in the next sequent, which concludes this case and completes the proof.

The last lemma used for proving our soundness result resembles Lemma 8.1, but it is stronger since it states the existence of strict successors in the observation relation. It can be proved thanks to Lemma 8.2. Lemma 8.3 For all sequents S, F G ∪ {ϕ} encountered by δ:

• either S ϕ;

• or for all γ 1 , γ 2 ∈ ϕ , there exists a sequent S, F G ∪ {ϕ } encountered by δ, and

γ 1 , γ 2 ∈ ϕ ⊆ O, such that γ 1 , γ 2 ⇒ + S 2 γ 1 , γ 2 .
Proof We proceed by (strong) induction on the length of the proof δ and case analysis. Depending on the first rule of δ that is applied to the sequent S, F G ∪ {ϕ}:

• if the rule is [Reduce] then there are two subcases:

if S ϕ then this case is proved;

-if ϕ ⊆ f for some f ∈ F : Then, f ∈ Φ since f is being used (by the present rule!) to discharge a goal. Thus, f ∈ F ∩ Φ. Using Lemma 8.2 we obtain the sequent S, F G ∪ {ϕ } and instance γ 1 , γ 2 ∈ ϕ ⊆ O such that γ 1 , γ 2 ⇒ + S 2 γ 1 , γ 2 , which proves this case; • if the rule is [Derive] or [Circularity]: using Lemma 7.1, for any γ 1 , γ 2 ∈ ϕ , there exists ϕ ∈ ∆ h (ϕ) and γ 1 , γ 2 ∈ ϕ such that γ 1 , γ 2 ⇒ S 2 γ 1 , γ 2 .
Moreover, the goal ϕ is the current goal of a future rule application in δ and is the origin of a proof δ strictly shorter than δ. Using the induction hypothesis, there exists the sequent S, F G ∪ {ϕ } and instance

γ 1 , γ 2 ∈ ϕ ⊆ O such that γ 1 , γ 2 ⇒ + S 2 γ 1 , γ 2 .
. By transitivity γ 1 , γ 2 ⇒ + S 2 γ 1 , γ 2 holds, which concludes the proof. Proof Pick any ϕ ∈ Γ (if Γ = ∅ the theorem is trivially true). Applying Lemma 8.3 generates two cases:

1. either S ϕ, which directly implies S |≡ ϕ;

2. or, for all γ 1 , γ 2 ∈ ϕ , there exists a sequent S, F G ∪ {ϕ } encountered by δ, and

γ 1 , γ 2 ∈ ϕ ⊆ O, such that γ 1 , γ 2 ⇒ + S 2 γ 1 , γ 2 .
We apply Lemma 8.3 to the latter sequent, which generates two cases:

(a) S ϕ , which implies S |≡ ϕ . Then from γ 1 , γ 2 ∈ ϕ , there is an execution satisfying O ∧ ♦O, and by adding to it the prefix γ 1 , γ 2 ⇒ + S 2 γ 1 , γ 2 , the resulting execution also satisfies O ∧ ♦O. Thus, from the (arbitrary) γ 1 , γ 2 ∈ ϕ there is an execution satisfying O ∧ ♦O, meaning S |≡ ϕ;

(b) or for all γ 1 , γ 2 ∈ ϕ , there exists a sequent S, F G ∪ {ϕ } encountered by δ, and

γ 1 , γ 2 ∈ ϕ ⊆ O, such that γ 1 , γ 2 ⇒ + S 2 γ 1 , γ 2 .
Applying Lemma 8.3 to the latter sequent generates two cases. . . It is not hard to see that in the first case we will be able to prove S |≡ ϕ like in item 2(a) above, and in the second one, another application of Lemma 8.3 will generate yet two more cases. . . This repetitive process may never terminate for a goal ϕ, but it proves S |≡ ϕ in one of two possible ways:

• the first one assumes that, after finitely many applications of Lemma 8.3, a subgoal ϕ (n) satisfying S ϕ (n) is found. Thanks to Lemma 8.3, from any γ 1 , γ 2 ∈ ϕ there is a finite execution e than leads into some instance γ • the second one assumes the contrary: there is no finite number of applications of Lemma 8.3 after which a subgoal ϕ (n) satisfying S ϕ (n) is found. In this case, the infinitely many applications of Lemma 8.3 build an infinite execution

(n) 1 , γ (n) 2 ∈ ϕ (n) . And since S |≡ ϕ (n) , starting from the instance γ (n) 1 , γ (n) 2 ∈ ϕ (n) ,
γ 1 , γ 2 ⇒ + S 2 γ 1 , γ 2 ⇒ + S 2 • • • ⇒ + S 2 γ (n) 1 , γ (n) 2 ⇒ + S 2 • • • , starting from any arbitrarily chosen γ 1 , γ 2 ∈ ϕ , such that O is met infinitely many times, as γ 1 , γ 2 ∈ ϕ ⊆ O, γ 1 , γ 2 ∈ ϕ ⊆ O, . . . , γ (n) 1 , γ (n) 2 ∈ ϕ (n) ⊆ O, .
. . , which implies that our execution satisfies O ∧ ♦O; thus, S |≡ ϕ holds.

In both cases, this process leads to establishing S |≡ ϕ, and ϕ ∈ Γ was chosen arbitrarily, thus, S |≡ Γ holds.

Remark 8.1 For soundness it is not essential that the [Circularity] ϕ actually adds the current goal ϕ to the current set of circular hypotheses F . What does matter is that, whenever ϕ is added to F , then ϕ ⊆ Ω . We use this observation in our implementation of the proof system to reduce the number of stored hypotheses.

We now show that the circular proof system, when it terminates, always provides an answer (positive or negative) to the question of whether S |≡ Γ holds. Thus, in addition to soundness we have a weak completeness result. The result is "weak" because it assumes termination of the proof system.

Given a a semantics S and set of goals Γ, the proof system terminates successfully when it returns a proof. The proof system terminates unsucessfully when its has a finite, maximal execution that is not a proof -we call such an execution a disproof. This happens when the proof system is "stuck": in the current sequence S, F G no rule of the system can be applied because the side-conditions of the rules are not satisfied. Then, dy definition, the proof system terminates on Γ if it terminates sucessfully or unsucessfully. Weak completeness then says that if a set of goals Γ is valid, all the goals in the set are satisfiable, and the proof system terminates on Γ, then it terminates successfully.

For this we need the following adaptation to the notion of derivative:

∆(ϕ) = {ϕ | ϕ ⇒ s S ϕ ∧ ϕ = ∅},
which means that only the satisfiable patterns are kept when computing derivatives. We also need:

Assumption 3 For all patterns ϕ of L, if ∆ S (ϕ) = {ϕ} then there is π ⇒ ⇒ ⇒ π ∈ S such that ∆ S (ϕ) = ∆ {π⇒ ⇒ ⇒π} (ϕ), and for all configurations γ, γ of L, if γ ⇒ S γ and γ ⇒ S γ then γ, γ / ∈ O.
Both assumptions regard the language L of interest. The first says that, whenever a the derivative of pattern is the pattern itself, then the only rule that contributes to this derivative is of the form rules π ⇒ ⇒ ⇒ π. Remember (Assumption 2) that such rules were included in the semantics S for technical reasons in order to transform terminal configurations into self-looping ones (ultimately, because we deal with LTL over infinite sequences). Our first asssumption then says that, except for the rules, π ⇒ ⇒ ⇒ π were added to the semantics, all the other rules "change" at least "something" in a pattern; ie., rules that do not change anything in the semantics of a language are useless. Regarding the second of the above assumptions, it says that self-looing configurations and non self-looping ones cannot be observationally equivalent. As observed before, the self-looping configurations are (formerly) terminal configurations that were transformed into self-looping ones by including the rules of the form π ⇒ ⇒ ⇒ π in the semantics S. Thus, our second assumption actually says that configurations where the code to be executed is finished, and configurations where there is still code to execute, cannot be observationally equivalent, which is also a reasonable constraint on equivalence.

Theorem 8.2 (weak completeness ) If S |≡ Γ and for all ϕ ∈ Γ it holds that ϕ = ∅, and the proof system terminates on Γ then S Γ.

Proof By contradiction: assume the hypotheses hold but not the conclusion, i.e., S Γ. Thus, the proof system terminates with a disproof δ, i.e., a sequence of rule applications that is not a proof and after which no rule can be applied. Let S, F G be the sequent resulting after δ. Thus, G = ∅, and for all ϕ ∈ G, ϕ ⊆ O (otherwise, [Circularity] would be applicable), and ∆ h (ϕ) = {ϕ} for h ∈ {l, r} (otherwise, [Derive] would be applicable). We choose any ϕ ∈ G. Since both [Circularity] and [Derive] rules compute derivatives, there exists ϕ 0 ∈ Γ and a symbolic execution

ϕ 0 ⇒ s S 2 • • • ⇒ s S 2 ϕ n = ϕ.
The symbolic execution is feasible, since we have assumed that only satisfiable patterns are kept in the derivatives. Moreover, ϕ n ⊆ O, thus, we can choose γ, γ ∈ ϕ \ O. Hence, we can apply Corollary 5.2 and find a concrete execution γ

0 , γ 0 ⇒ S 2 • • • ⇒ s S 2 γ n , γ n = γ, γ such that for all i = 0, n -1, γ i , γ i ∈ ϕ i , and γ n , γ n ∈ ϕ n \ O.
Next, due to the definition of the language L 2 , by projecting the above concrete execution of L 2 on its left and right components we obtain the two executions e γ 0 ⇒ * S γ and e γ 0 ⇒ * S γ of L. Let ϕ = π, π ∧ ∧ ∧ φ, then, γ ∈ π ∧ ∧ ∧ φ and γ ∈ π ∧ ∧ ∧ φ . From ∆ l (ϕ) = ∆ r (ϕ) = {ϕ} we obtain ∆ S (π ∧ ∧ ∧ φ) = {π ∧ ∧ ∧ φ} and ∆ S (π ∧ ∧ ∧ φ) = {π ∧ ∧ ∧ φ}, thus, Using Assumption 3, both these derivarives were obtained by applying rules of the form π ⇒ ⇒ ⇒ π ∈ S. Thus, there are transitions γ ⇒ S γ and γ ⇒ S γ in L, and the finite executions e, e can be extended into infinite ones

e γ 0 ⇒ * S γ ⇒ S γ • • • ⇒ S γ • • • and e γ 0 ⇒ * S γ ⇒ S γ • • • ⇒ S γ • • •
, and since L is deterministic, e, resp. e is the only infinite execution of L starting in γ 0 , resp. in γ 0 .

Moreover, the infinite executions in L 2 starting in γ 0 , γ 0 coincide with sequences obtained by interleaving transitions of e and e . It is thus enough consider any such interleaving, denoted hereafter by e e , and show that it satisfies ♦ ¬O.

There are two cases:

• in e e , both e and e have reached γ, resp. γ . Thus, e e has an infinite suffix that only repeats the instance γ, γ ∈ ϕ \ O, which is does not satisfy O; thus, e e |= ♦ ¬O.

• in e e , only one of the components, say, e, has reached γ. Thus, e e has an infinite suffix that only repeats an instance of the form γ, γ , for some configuration γ that does not have a transition γ ⇒ S γ (that would contradict the unicity of the infinite execution e starting in γ 0 ). By Assumption 3, we have γ, γ / ∈ O and since e e ends up by only repeating γ, γ , we have e e |= ♦ ¬O again.

Recapitulating, we have obtained a goal ϕ 0 ∈ Γ and an instance γ 0 , γ 0 ∈ ϕ 0 , and two infinite executions e and e of L, starting in γ 0 , and γ 0 , respectively, such that any infinite execution of L 2 starting in γ 0 , γ 0 is of the form e e for some interleaving of e, e ; and any such infinite execution e e satisfies ♦ ¬O. According to Definition 7.1 this means γ 0 ∼ γ 0 , and according to Definition 7.3, this means S |≡ϕ 0 . Hence, S |≡Γ, which is in contradiction to the hypothesis S |≡ Γ of our theorem. The contradiction was obtained by assuming S Γ, hence, S Γ holds, which concludes the proof.

Together, the soundness and weak completeness say results say that, if the proof system applied to a given set of goals terminates, then termination is successful if and only if the set of goals is valid. That is, when it terminates, the proof system correctly solves the programequivalence problem as we have stated it. Of course, termination cannot be guaranteed, because the equivalence problem is undecidable. It does terminate on goals in which both programs terminate (because eventually the set of derivatives does not change the goals and no rule can be applied any more) and also for goals in which the programs does not terminate, but behave in a certain "regular" way, as shown in the examples below.

Example 8.1 We start by illustrating the use of the deductive system on the equivalence of stream programs since it does not require unification, hence it is a bit easier. The equivalence we want to prove is that from Example 1.2: blink is equivalent to zip(zero, one). This is written as the equivalence formula

blink k spec 1 specs Y 1 out cfg , zip(zero, one) k spec 2 specs Y 2 out cfg ∧ ∧ ∧ Y 1 = Y 2 (2)
where spec 1 is blink → λ() .0:1:blink and spec 2 is the map zero → λ() .0:zero one → λ() .1:one zip → λ(xs, ys) .zip( ys , hd( xs )) Note that the contents of the cells specs is not changed during the execution of the program. The observation relation is given by

Ω = { C 1 k spec 1 specs Y 1 out cfg , C 2 k spec 2 specs Y 2 out cfg } ∧ ∧ ∧ Y 1 = Y 2
where C 1 and C 2 are two arbitrary stream programs. In words, two configurations are observational equivalent iff the corresponding output cells out have equal contents.

The equivalence formula (2) is the unique goal in G we start with. We first apply [Circularity] for the program blink (i.e., in the proof system, the derivative ∆ l () is applied), which loads the definition of blink in the k cell, and adds (2) to the set of circular hypotheses F . We then apply [Derive] twice, which writes in the corresponding output cell the two head elements of the stream, and produces the following goal:

blink k spec 1 specs 0 : 1 : Y 1 out cfg zip(zero, one) k spec 2 specs Y 2 out cfg ∧ ∧ ∧ Y 1 = Y 2 (3)
Not that the contents of the output cell in the first configuration has changed. Next, by applying Derive several times with the heating/cooling rules that compute the arguments of zip(zero, one), we get blink k spec 1 specs 0 : 1 :

Y 1 out cfg zip(0 : zero, 1 : one) k spec 2 specs Y 2 out cfg ∧ ∧ ∧ Y 1 = Y 2 (4)
Several other applications of Derive proceed with loading the definition of zip in the k cell, applying heating/cooling rules for hd(zero), adding content to the output cell, and computing new arguments of zip: blink k spec 1 specs 0 : 1 : Y 1 out cfg zip(1 : one, 0 : zero) k spec 2 specs 0 :

Y 2 out cfg ∧ ∧ ∧ Y 1 = Y 2 (5)
The above process is repeated with the new instance of zip, which produces the following goal:

blink k spec 1 specs 0 : 1 : Y 1 out cfg zip(0 : zero, 1 : one) k spec 2 specs 0 : 1 :

Y 2 out cfg ∧ ∧ ∧ Y 1 = Y 2 (6)
To conclude the proof, we note that ( 6) is an instance of (2) by applying the substitution

{Y 1 → 0 : 1 Y 1 , Y 2 → 0 : 1 Y 2 }. Hence, (6) ⊆ (2)
, and the Reduce discharges the (unique) current goal [START_REF] Chaki | Regression verification for multi-threaded programs[END_REF], and Axiom concludes the proof.

Example 8.2 We show the application of our proof system for proving the equivalence of for and while programs formalised as the validity of the following formula, with A, B : Int, S : Stmt, I : Id and M : Map Considering A, B to be integers instead of expressions is not a restriction, since, if A and B were artihmetical expressions, the strictness attributes for the for, assigment, and <= would be applied first and would transform A, B into integers anyway. This allows us to simplify the original equivalence formula , given in Example 7.2, into the following one, based on the fact that isModified (A, S ) = isModified (B , S ) = false:

for I from A to B do{ S } k , M env cfg I = A ;while I <= B do{ S ; I = I + 1 } k , M env cfg ∧ ∧ ∧ ¬ Bool isModified (I , S ) (7)
The observation relation is given by the set

Ω = { C 1 k M env cfg , C 2 k M env cfg ∧ ∧ ∧M = M ap M }.
The relation says that two configurations are observationally equivalent iff they have equal environments.

In order to prove the goal (7) with our proof system we start with a set of goals G consisting of [START_REF] Leroy | Formal verification of a realistic compiler[END_REF] and

C (for I from A to B do{ S }) k , M env cfg C (I = I + 1;while I <= B do{ S ; I = I + 1 }) k , M env cfg ∧ ∧ ∧ ¬ Bool isModified (I , C ) ∧ Bool lookup(M , I ) = A ( 8
)
where C is a variable of sort Code. Remember that Code is a sort that includes all statements and arithmetical and Boolean expressions, that • denotes the empty code, and that code sequencing is denoted by .

In the sequel we show the application of the rules of our proof system to the chosen set of goals G. The first rule applied to ( 7) is [Circularity], by which ( 7) is added to the hypotheses H and is replaced by a goal obtained by applying the semantical rule for the for statement, which gives:

I = A ;if I <= B then S ;for I from A + Int 1 to B do {S} else skip} k , M env cfg I = A ;while I <= B do{ S ; I = I + 1 } k , M env cfg ∧ ∧ ∧ ¬ Bool isModified (I , S )
We now apply the sequence of rules [Circularity], [Derive], [Circularity], without adding new hypotheses5 , which replaces the above goal with the following one, obtained by applying the semantics of assignment to both sides of the formula and then the semantical rule for the while statement: Next6 , the heating rules for the if statement and the _ <= _ operation, followed by the cooling rules, and finally the rules that conclude the evaluation of the if statement result in the two following subgoals:

skip k , update(M, I, A) env cfg skip k , update(M, I, A) env cfg ∧ ∧ ∧ ¬ Bool isModified (I , S ) ∧ Bool ¬ Bool A ≤ Int B S ;for I from A + Int 1 to B do {S} k , update(M, I, A) env cfg S ; I = I + 1 ; while I <= B do{ S ; I = I + 1 } k , update(M, I, A) env cfg ∧ ∧ ∧ ¬ Bool isModified (I , S ) ∧ Bool A ≤ Int B
The first subgoal is trivially valid and is eliminated by the [Reduce] rule using the base entailment . By applying the semantical rule for statement sequencing, which rewrites ; to , for the second one, we get a new goal

∧ ∧ ∧ ¬ Bool isModified (I , S ) ∧ Bool A ≤ Int B (9)
which is eliminated by the the [Reduce] rule since it is an instance of the goal (8) (by using the substitution C ← S, M ← update(M, I, A), and by using the equality lookup(I , update(M , I , A)) = A).

To conclude the proof we also need to eliminate the goal [START_REF] Necula | Translation validation for an optimizing compiler[END_REF]. This elimination amounts to unifying the code C with all possible left-hand sides of rules in the semantics of imp. We only give a subset of all the cases, since considering all cases may be overlong for the reader's patience (but not so for a computer). We first consider the case where S is unified with statements:

• C ← skip: by applying the semantical rules for skip (which rewrites it to •), then the rule that consumes the empty code •, and finally the rule sequence that evaluates I + 1 in the goal's right-hand side, the goal (8) becomes the following one, which is implied by the initial goal [START_REF] Leroy | Formal verification of a realistic compiler[END_REF] and is eliminated by [Reduce]: The other subgoal is similar, but with S 2 instead of S 1 and B = Bool false in the condition, which is also an instance of the goal [START_REF] Necula | Translation validation for an optimizing compiler[END_REF].

for I from A to B do{ S } k , M env cfg I = A ;while I <= B do{ S ; I = I + 1 } k , M env cfg ∧ ∧ ∧ ¬ Bool isModified (I , S ) ∧ Bool lookup(M , I ) = A • C ←
if B does not have the sort Bool then it has the sort BExp. Then, the only rule that our goal can be unified with is the heating rule for if, which generates the following goal:

(B if then S 1 else S 2 ) (for I from A + Int 1 to B do {S}) k , M env cfg (B if then S 1 else S 2 ) (I =I + 1 ;while I <= B do {S; I =I + 1}) k , M env cfg ∧ ∧ ∧ ¬ Bool isModified (I , S 1 ) ∧ Bool ¬ Bool isModified (I , S 2 )
which is an instance of (8) with S ← (B if then S 1 else S 2 ).

• C ← while B do S . The rule for while transforms (8) into an instance of itself under the substitution C ← (if B then S ; I + 1 ; while B do S else skip).

• C ← for I from A to B do S . The rule for for transforms (8) into an instance of itself under the substitution C ← (I = A ; if B then S ; I + 1 ; for I from A to B do S else skip).

• C ← X for some identifier X, which amounts to unification with the rule for programvariable lookup. That rule transforms our goal into an instance of itself with C ← lookup(M , X , I ).

• C ← X = A for some identifier X and arithmetical expression A . Similar to the case of if, there are subcases depending on whether has sort Int, or does not have sort Int but has sort AExp.

in the first case the rule for variable assignment transforms (8) into an instance of itself with C ← • and M → update(M , X , I );

in the second case, the heating rule for variable assignment transforms 8) into an instance of itself with C ← (A I = ).

There remain to consider the cases where C is code but is not a statement. The goal (8) can be unified with left-hand sides of semantical rules:

• C ← C 1 C 2 : then unification may be performed with both heating and cooling rules.

-We first illustrate the situation with the cooling rule for the if statement, which was explicitly given in Section 2.1; the case for all the other cooling rules is completely similar. In the considered case, C 1 ← B and C 2 ← if then S 1 else S 2 C for some code C , and the cooling rule transforms (8) into an instance of itself with

C ← if B then S 1 else S 2
C .

-Regarding unification with heating rules, this may only happen when the left-hand side of the rule is of the form C 1 C 2 k M env cfg , and the right-hand side has the form

(C 1 C 2 ) C 2 k M env cfg ; the application of this rule transforms (8) into an instance of itself with C ← C 1 C 2 .
• C is an arithmetical expression or a Boolean expression. Then, again, unification may be performed with both heating and cooling rules, in a completely similar many to what has been shown above.

Thus, in all possible cases, the goal goal ( 8) is transformed into an instance of itself and is eliminated from the set of goals. Since the other goal [START_REF] Leroy | Formal verification of a realistic compiler[END_REF] has been eliminated earlier, the proof system terminates sucessfully.

A Prototype Implementation

K [START_REF] Roşu | An Overview of the K Semantic Framework[END_REF] is a framework for defining the formal operational semantics of programming languages. One component of the framework is a compiler of K definitions to Maude [START_REF] Clavel | All About Maude, A High-Performance Logical Framework[END_REF] specifications. Programs of languages defined in K can thus be executed and analysed using Maude as the underlying rewriting engine. K also offers some support for symbolic computations, including a connection to the Z3 SMT solver [START_REF] De | Z3: An efficient SMT solver[END_REF]. We have used these components in a prototype tool implementing our deductive system for program equivalence. Here we describe how the proposed proof system is implemented for the imp and stream languages. This description is generic enough and can be seen as a methodology applicable to any language defined in K.

There are (at least) two approaches to implementing the proof system:

1. as an external procedure, which uses the K tool for computing derivatives of equivalence formulas only. The external procedure is then responsible all the other operations, including the searching for proofs;

2. directly in K, by performing all the operations in the proof system using the available K tools (for example, the underlying Maude search engine is used in searching for proofs). This requires extending the definition of the language of interest definitions with additional data structures, with semantical rules for storing circular hypotheses, and with rules for the entailment between these hypotheses and goals.

Since our approach is parametric in the language definition, observational relation, and basic entailment, in both cases we need a procedure that builds the definition of L 2 for a given L, and procedures for the basic entailment (S ϕ) and subsumption ( ϕ ⊆ f ). The basic entailment relation S 2 ϕ can be specified by means of a (finite) set of equivalence formulas E (in the same way that Ω specifies the observation relation O), and taking S 2 ϕ iff there is e ∈ E such that ϕ ⊆ e . The subsumption relation can be checked using Proposition 3.2 or Proposition 3.3.

For imp the set Ω will typically consist of formulas that say that a given set of program variables have the same values in both configurations, and E further requires that the two contents of the k cells are the same. For stream, Ω says that the two out cells have the same contents. By Proposition 3.1, the formulas f ∈ F and e ∈ E can always be stored in the form π ∧ ∧ ∧ σ ∧φ, which facilitates the checking of subsumptions based on Proposition 3.2 or Proposition 3.3. The validity of the implication from Proposition 3.2 is checked by calling the Z3 SMT solver. The substitution σ (ocurring in formulas of the form π ∧ ∧ ∧ σ ∧φ) is computed by inspecting the contents of the two configurations π and π .

We chose to implement the proof system for the two languages directly in K since this is the most straightforward approach and allows us to benefit from tools in the K framework. However, we had to make some compromises. Since the current Maude backend of K is a rewriting engine based on matching, we had to axiomatise symbolic statements instead of using unification for them. The main axiom says how a symbolic-statement variable S affects the environment M under a current condion φ:

S ••• k M env cfg ∧ ∧ ∧ φ ⇒ ⇒ ⇒ • ••• k followup(S, M, φ) env cfg ∧ ∧ ∧ φ
The function followup is axiomatised as well; its axiom says that S has no effect on a variables X that it does not modify: followup(S, (X → V M ), φ) = X → V followup(S, M, φ) when φ implies ¬isModified (X, S).

An equivalence formula ϕ π 1 , π 2 ∧ ∧ ∧ φ for imp is written in K as an imp configuration

p 1 k M 1 env cfg1 p 2 k M 2 env cfg2 φ cond
where the pattern π i is given by the contents of the cfg i cell and the condition φ is stored into a new cell called cond. The circularities F are stored into a new cell hypos. For each circularity f ∈ F , the subsumption relation ϕ ⊆ f is checked by means of two substitutions. The first one is a substitution σ from the contents of the cell k in f to the coresponding one in ϕ. Let f p 1 k M 1 env cfg1 p 2 k M 2 env cfg2 φ cond such an hypothesis in F and let ϕ be the current equivalence formula represented as above. For instance, if ϕ is given by ( 9) and f by (8), then σ is A ← A + Int 1. The expressions from the codomain of σ are evaluated in the current configuration; in this way, e.g., the program variables are replaced by their current values. Since the cell env includes only fresh variables, we have f σ equal to

p 1 k M 1 env cfg1 p 2 k M 2 env cfg2 φ σ cond
The second substitution σ is between the corresponding env cells such that M i σ = M i for i = 1, 2. Note that f σσ = ϕ does not hold in general, because usually φ σσ = φ does not. But if φ ∧ σ implies φ σ holds, which is checked by calling the SMT solver, then we obtain ϕ ⊆ f σ by Proposition 3.2 . Since f σ ⊆ f by Proposition 3.3, it follows that ϕ ⊆ f . This method for checking the subsumption relation is not specific to imp. For any other language definition the substitution σ is defined by structural induction on the language syntax and the substitution σ is computed by considering the rest of configurations. For instance, for the case of stream, only the substitution σ is required because the rest of configurations remain constant during the execution.

The efficiency of the implementation depends on how the [Circularity] and [Derive] rules are applied. In Remark 8.1 we noted that, for soundness, it is not necessary to always add the current goal ϕ to the hypotheses F when applying [Circularity]. Ideally, only those formulas actually subsequently used by [Reduce] rules should be added. Since there is no way of knowing in advance which circular hypotheses will be used in the future, we apply a heuristic when adding circular hypotheses. This is achieved by using labelled statements: each time two statements with the same label are at the top of the k cells, a set of rules decides which one of the following three cases holds for the current configuration and takes the corresponding action: whether it belongs to the observation relation, or it is a consequence of the circular hypotheses, or it must be added to the circular hypotheses.

The contents of the cell hypos at the end of a successful proof includes in fact new equivalences that the tool discovered during proving process. For instance, if the goal is morse ≈ f(morse), where then the following new equivalence is found:

1:f(1:zip(tl(morse), not(tl(morse)))) ≈ 1:zip(tl(morse),not(tl(morse))).

We also note that the stream example shows that the proof system introduced in this paper includes the one defined in [START_REF] Roşu | Circular coinduction -a proof theoretical foundation[END_REF] whenever behavioural equational specifications can be encoded as programming language definitions. However, the definition for the equivalence we introduced here is more general: the equivalence considered in [START_REF] Roşu | Circular coinduction -a proof theoretical foundation[END_REF] can be defined using the LTL formula pattern O while the one defined here uses ♦O.

Conclusion and Future Work

We have presented a definition for program equivalence, a logic that encodes this definition in its formulas, and a proof system for the logic, which is proved sound and weakly complete. A prototype implementation for the proof system in the K framework was also presented and illustrated on example of equivalent programs in languages from two different paradigms.

The proposed approach is generic: it does not depend on K and the language being defined in K, but requires a formal semantics of the language of interest as a term-rewriting system. The chosen equivalence relation is also parametric in a certain observation relation and requires that starting from configurations in the observartion relation, configurations in the observarion relation will be encountered again. We show the approach is applicable for concrete and symbolic programs and for terminating and non-terminating ones.

Future Work

We are currently applying our deductive system for proving the correctness of a compiler between two languages (as part of another project we are involved in). The source language is a stack-based language with control structures (loops, conditionals, dynamical function definitions). The target is also stack-based but only has (possibly, conditional) jumps. The correctness of the compiler amounts to proving the equivalence of several pairs of symbolic programs; in each pair, one component denotes a source-language control structure, and the other component is the translation of that control structure in the target language using jumps. We are also planning to combine our program-equivalence verification with matching logic [START_REF] Roşu | Checking reachability using matching logic[END_REF], a language-independent logic for programs written in languages with a rewrite-based semantics. The idea is to prove matching logic properties on programs in the source language, and guarantee, via the compiler's correctness that the compiled programs in the target language satisfy those properties as well.

  hd( x : xs ) ≈ x ; tl( x : xs ) ≈ xs ; zero ≈ 0 : zero; one ≈ 0 : one; blink ≈ 0 : 1 : blink; zip( xs , ys ) ≈ hd( xs ) : zip( ys , tl( xs ));

Int:

  := domain of integer numbers (including operations) Bool ::= domain of boolean constants (including operations) Id ::= domain of identifiers AExp ::=Int | Id | AExp / AExp [strict] | AExp * AExp [strict] | AExp + AExp [strict] | (AExp) BExp ::=Bool | AExp <= AExp [strict] | not BExp [strict] | BExp and BExp [strict(1)] | (BExp) Stmt :: = skip | Stmt ; Stmt | Id = AExp | if BExp then Stmt else Stmt [strict(1)] | { Stmt } | while BExp do Stmt | for Id from AExp to AExp do Stmt [strict(2, 3)]

Figure 2 :Figure 3 :

 23 Figure 2: K Semantics of IMP

Figure 4 :

 4 Figure 4: K Syntax of stream

CodekFigure 5 :

 5 Figure 5: stream configurations.

Figure 6 :

 6 Figure 6: K Semantics of stream.

  Var ) then we write ρ |= b iff bρ = D true , where bρ is the Boolean value obtained by applying ρ to b. For simplicity, we often write true, false instead of D true , D false . 3. A set S of rewrite rules l ∧ ∧ ∧ b ⇒ ⇒ ⇒ r, whose formal definition is given later in the section.

Remark 3 . 2

 32 The conditions var (π ) ∩ var (π ∧ ∧ ∧ φ) = ∅ and yσ = y for all y ∈ var (π ) required by Proposition 3.1 and Proposition 3.2 can be easily obtained by a variable renaming. Proposition 3.3 Let π ∧ ∧ ∧ φ and π ∧ ∧ ∧ φ two patterns such that there is a substitution σ with

Definition 5 . 1 ( 1 . 5 . 2

 51152 Symbolic transition relation) ϕ ⇒ s S ϕ iff ϕ π ∧ ∧ ∧ φ, there is a rule α (l ∧ ∧ ∧ b ⇒ ⇒ ⇒ r) ∈ S with var (l) ∩ var (π) = ∅and such that l, π are concretely unifiable, and ϕ = rσ l π ∧ ∧ ∧ (φ ∧ b)σ l π , where σ l π is unique, most general symbolic unifier of l, π constructed as in the proof of Lemma 4.Definition The derivative of a pattern is the set of patterns that can be obtained by one symbolic execution step:

Lemma 5 . 1

 51 If γ ⇒ S γ and γ ∈ ϕ then there exists ϕ such that γ ∈ ϕ and ϕ ⇒ s S ϕ .Proof Let ϕ π ∧ ∧ ∧ φ. From γ ⇒ S γ we obtain the rule α l ∧ ∧ ∧ r ⇒ ⇒ ⇒ b and the valuation ρ : Var → T such that γ = lρ, bρ = true, and γ = rρ. From γ ∈ ϕ we obtain the valuation µ : Var → T such that γ = πµ and φµ = true. Thus, l and π are concretely unifiable (by their concrete unifier ρ| var (l) µ| var (π)

Lemma 5 . 2

 52 If γ ∈ ϕ and ϕ ⇒ s S ϕ then there exists γ ∈ T Cfg such that γ ⇒ S γ and γ ∈ ϕ . Proof From ϕ ⇒ s S ϕ with ϕ π ∧ ∧ ∧ φ and α l ∧ ∧ ∧ r ⇒ ⇒ ⇒ b we obtain ϕ = rσ l π ∧ ∧ ∧ (φ ∧ b)σ l π . From γ ∈ ϕ we obtain η : Var → T such that γ = (rσ l π )η and ((φ ∧ b)σ l π )η = true. We extend σ l π to var (ϕ, α) by letting it be the identity on var (ϕ, α) \ var (l, π). Let ρ : Var → T be defined by xρ = x(σ l π η) for all x ∈ var (ϕ, l), and xρ = xη for all x ∈ Var \ var (ϕ, l), and let γ lρ. From γ = (rσ l π )η and the definition of ρ we obtain γ = rρ. From ((φ ∧ b)σ l π )η = true we obtain b(σ l π η) = true, i.e., bρ = true, which together with γ lρ and γ = rρ gives γ ⇒ S γ . There remains to prove γ ∈ ϕ .

  LTL formulas are generated by the grammar ψ ::= true | p | ψ | ψ ∧ ψ | ¬ψ | ψ U ψ for all p ∈ P . Standard abbreviations are false ¬true, ψ 1 ∨ ψ 2 ¬(¬ψ 1 ∧ ¬ψ 2 ), ♦ψ true Uψ, and ψ ¬♦¬ψ. Given an execution e s 0 , . . . , s n , . . . of a Kripke structure (S, ⇒, P, λ, S i ) and an LTL formula ψ, the satisfaction relation e |= ψ is inductively defined over the structure of ψ as follows: • e |= true; • e |= p iff p ∈ λ(s 0 ); • e |= p iff e 1 |= p • e |= ψ 1 ∧ ψ 2 if e |= ψ and e |= ψ 2 ;

Theorem 8 . 1 (

 81 soundness) Let Γ be a finite set of equivalence formulas. If S Γ then S |≡Γ.

  an infinite execution e satisfying O ∧ ♦O exists. The concatenation ee also satisfies O ∧ ♦O. Thus, from the arbitrarily chosen γ 1 , γ 2 ∈ ϕ en execution satisfying O ∧ ♦O exists, meaning S |≡ ϕ holds.

  if I <= B then S ;for I from A + Int 1 to B do {S} else skip} k , update(M, I, A env cfg if I <= B then S ; I = I + 1 ;while I <= B do{ S ; I =I + 1 }else skip k , update(M, I, A env cfg ∧ ∧ ∧ ¬ Bool isModified (I , S )

S

  (for I from A + Int 1 to B do {S}) k , update(M, I, A) env cfg S (I = I + 1 ; while I <= B do {S ; I = I + 1}) k , update(M, I, A) env cfg

  morse ≈ 0:1:zip(tl(morse), not(tl(morse))); not( xs ) ≈ neg(hd( xs )):not( xs ); f( xs ) ≈ hd( xs ):neg(hd( xs )):f(tl( xs )); neg( x ) := 1 x = Int 0 0

  variables of sort Id and A of sort Int is nonlinear because Y occurs twice. Moreover, it contains the nonvariable data terms A + Int 1. It is thus transformed into the pattern

  {S 1 ; S 2 } for some statements S 1 , S 2 : the rule rewriting ; to produces an instance of the goal (8) itself, with the substitution C ← S 1 S 2 , which is then eliminated by [Reduce]. • C ← {S } for some statement S : the rule for {_} elimination produces an instance of the goal (8) itself, with the substitution C ← S , which is then eliminated by [Reduce]. • C ← if B then S 1 else S 2 , for some Boolean expression B and statements S 1 , S 2 : there are two subcases, depending on whether B has the sort Bool , or does not have the sort Bool but has sort BExp: -if B has the sort Bool then one can directly apply the rules for if and obtain two subgoals: one is S 1 (for I from A + Int 1 to B do {S}) k , M env cfg S 1

(I = I + 1 ; while I <= B do {S ; I = I + 1}) k , M env cfg ∧ ∧ ∧ ¬ Bool isModified (I, S 1 ) ∧ Bool ¬ Bool isModified (I, S 2 ) ∧ Bool B = Bool true

(where we used isModified (I, if B then S 1 else S 2 ) = isModified (I, S 1 ) ∨ Bool isModified (I, S 2 )). This is an instance of the goal

[START_REF] Necula | Translation validation for an optimizing compiler[END_REF]

and is eliminated by [Reduce] 7 .

We have developped the approach for the equivalence of programs belonging to one language L for simplicity reasons. However, considering two languages L and L poses no conceptual difficulty and can even be reduced to the one-language case. Indeed, any program in language L and any program in language L are also programs in the language L L , i.e, in the disjoint union of the two languages. This union obtained by (possibly) renaming some common language constructions to avoid ambiguity.

In the K terminology the sort Code is called K. We changed its name in order to avoid confusions due to name overloading.

even though the standard notion of most general unifier in algebraic specifications and rewriting is a different one.

f ∈ Σ \ Σ Data because the contrary would mean that t 1 has a Data sort, in contradiction with the lemma's hypotheses.

which is sound thanks to Remark 8.1. In the sequel, whenever [Circularity] is applied, by default it does not add new hypotheses.

In the sequel we mention only the semantical rules used in the sequence of rules [Circularity] and [Derive] that is applied to obtain the next goal.

in the sequel, whenever (8) is transformed into an instance of itself, we omit the sentence "and is eliminated by [Reduce]".

Parc scientifique de la Haute-Borne 40 avenue Halley -Bât A -Park Plaza 59650 Villeneuve d'Ascq Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr ISSN 0249-6399

Acknowledgments This work was partially supported by Contract 161/15.06.2010, SMISC-SNR 602-12516.