Observational proofs by rewriting.
Observability concepts contribute to a better understanding of software correctness. In order to prove observational properties, the concept of Context Induction has been developed by Hennicker (Hennicker, Formal Aspects of Computing 3(4) (1991) 326-345). We propose in this paper to embed Context Induction in the implicit induction framework of (Bouhoula and Rusinowitch, Journal of Automated Reasoning 14(2) (1995) 189-235). The proof system we obtain applies to conditional specifications. It allows for many rewriting techniques and for the refutation of false observational conjectures. Under reasonable assumptions our method is refutationally complete, i.e. it can refute any conjecture which is not observationally valid. Moreover this proof system is operational: it has been implemented within the Spike prover and interesting computer experiments are reported.
Introduction
Observational concepts are fundamental in formal methods since for proving
the correctness of a program with respect to a specication it is essential to
be able to abstract away from internal implementation details. Data objects
can be viewed as equal if they cannot be distinguished by experiments with
observable result. The idea that the semantics of a specication must describe
the behaviour of an abstract data type as viewed by an external user, is due
to [14]. Though a lot of work has been devoted to the semantical aspects of
observability (see [4] for a classication), few proof techniques have been studied
[35,7,25,24], and even less have been implemented. More recently there has
been an increasing interest for behavioural/observational proofs with projects
such as CafeOBJ (see e.g. [27]) and the new approach for validation of object-oriented
software that is promoted by B. Jacobs [18,19].
In this paper we propose an automatic method for proving observational properties
of conditional specications. The method relies on computing families of
Email addresses: Adel.Bouhoula@supcom.rnu.tn (Adel Bouhoula),
rusi@loria.fr (Michael Rusinowitch).
Preprint submitted to Elsevier Science
well chosen contexts, called critical contexts, that \cover" in some sense all observable
ones. These families are applied as induction schemes. Our inference
system basically consists in extending terms by critical contexts and simplifying
the results with a powerful rewriting machinery in order to generate new
subgoals. An advantage of this approach is that it allows also for disproving
false observational conjectures. The method is even refutationally complete
for an interesting class of specications. From a prototype implementation
on top of the Spike prover [9] computer experiments are reported. The given
examples have been treated in a fully automatic way by the program.
Related works
Hennicker [16] has proposed an induction principle, called context induction,
which is a proof principle for behavioural abstractions. A property is observationally
valid if it is valid for all observable experiments. Such experiments
are represented by observable contexts, which are context of observable sort
over the signature of a specication where a distinguished subset of its sorts
is specied as observable. Hence, a property is valid for all observable experiments
if it is valid for all corresponding observable contexts. A context c is
viewed as a particular term containing exactly one variable; therefore, the sub-term
ordering denes a noetherian relation on the set of observable contexts.
Consequently, the principle of structural induction induces a proof principle
for properties of contexts of observable sort, which is called context induction.
This approach provides with a uniform proof method for the verication of
behavioural properties. It has been implemented in the system ISAR [3]. How-
ever, in concrete examples, this verication is a non trivial task, and requires
human guidance: the system often needs a generalization of the current induction
assertion before each nested context induction, so that to achieve the
proof.
Malcolm and Goguen [25] have proposed a proof technique which simplies
Hennicker proofs. The idea is to split the signature into generators and dened
functions. Proving that two terms are behaviourally equivalent, comes to prove
that they give the same result in all observable contexts built from dened
functions, provided that the generators verify a congruence relation w.r.t.
behavioural equivalence. This proof technique is an e-cient optimization of
Hennicker proofs.
Bidoit and Henniker [6] have investigated how a rst order logic theorem
prover can be used to prove properties in an observational framework. The
method consists in computing automatically some special contexts called crucial
contexts, and in enriching the specication so that to automatically prove
observational properties. But this method was only developed for the proof
of equations and for specications where only one sort is not observable. Be-
sides, it fails on several examples (cf. Stack example), where it is not possible
to compute crucial contexts.
Bidoit and Hennicker [7] have also investigated characterization of behavioural
theories that allows for proving behavioural theorems with standard proof
techniques for rst order logic. In particular they propose general conditions
under which an innite axiomatization of the observational equality can be
transformed into a nitary one. However, in general there is no automatic
procedure for generating such a nite axiomatization of the observational equality

Puel [30] has adapted Huet-Hullot procedure for proof by consistency w.r.t.
the nal model. Lysne [24] extends Bachmair's method for proof by consistency
to the nal algebra framework. The proof technique is based on a special
completion procedure whose idea is to consider, not only critical pairs emerging
from positioning rewrite rules on equations, but also those emerging from
positioning equations on to rewrite rules. This approach is restricted to equations
and requires the ground convergence property of the axioms in order
to be sound (in our case, ground convergence is needed only for refutational
completeness).
A preliminary version of this paper has been presented in march 1998 [2].
In comparison the system we study here admits more powerful simplication
techniques. For instance contextual simplications are now allowed with conditional
rules.
There exists more recent related works [12,26]. For instance the circular coinductive
rewriting approach of Goguen and Rusu [12] is also based on computing
special contexts. However these contexts cannot be used in general for
refutation. Our approach also allows for more simplication techniques since
e.g. each clause which is smaller than the current subgoal can be used as an
induction hypothesis and contextual rewriting is available. Unlike others we
also allow specications with relations between constructors.
In section 3 we introduce our approach with a simple example. Then we give
in section 4 the concepts of algebraic specications and rewriting that are
required in order to describe the observational semantics in section 4, our
induction schemes in section 6 and inference system in section 7. Finally we
report computer experiments with a prototype implementation in section 8.
Future extensions of the technique are sketched in the conclusion.
3 An object-oriented example
Observational specication techniques are well adapted to the description of
object-oriented systems where non observable sorts are used to model the states
of objects, and states can be observed only by applying methods on
their attributes. Hence observational techniques allow to describe systems in
an abstract way, hiding implementation details. Objects are considered as behaviourally
equivalent whenever they produce the same reactions to the same
observable experiments (actions, transitions, messages Consider for instance
a simple class of points given with their cartesian coordinates.
class Point
private distance : nat
methods create
incry
decry
We assume that the point instances are initially located at the origin (0;
and they are \moved" by methods incrx, incry (resp decx, decy) for incrementing
coordinates. Two accessors getx, gety allow to
consult the public attributes x,y. A Point instance also comes with a private
attribute whose value is the distance it has covered since its creation. The
distance is incremented after each call to incrx or incry. Given two fresh instances
of the class, P and P' we can prove that
are behaviourally equivalen-
t, although their attributes are not identical. The behavioural equivalence
is dened here using observable contexts. A context is a term describing an
experience to be applied to an object. For instance getx( ) is an observable
context for the point class. Our approach relies on computing families of well
chosen contexts, called critical contexts. These families cover in some sense all
observation contexts and are applied as induction schemes. In the Point example
the critical contexts are getx(z point ); gety(z point ). Our inference system
basically consists in applying critical contexts to conjectures and simplifying
the results by rewriting rules in order to generate new subgoals. For instance
proving the behavioural equivalence A  B of A and B reduces to the proof of
getx(B) and gety(A)  gety(B). Both subgoals can be simplied
to tautological equations and this nishes the proof.
4 Basic notions
We assume that the reader is familiar with the basic concepts of algebraic
specications [37], term rewriting and equational reasoning. A many sorted
signature  is a pair (S; F ) where S is a set of sorts and F is a set of function
symbols. For short, a many sorted signature  will simply be denoted by F . We
assume that we have a partition of F in two subsets, the rst one, C, contains
the constructor symbols and the second, D, is the set of dened symbols. Let
X be a family of sorted variables and let T (F; X) be the set of sorted terms.
stands for the set of all variables appearing in t. A term is linear if all
its variables occur only once in it. If var(t) is empty then t is a ground term.
The set of all ground terms is T A be an arbitrary non-empty set,
and let Fg such that if f is of arity n then f A is a function
from A n to A. The pair (A; FA ) is called a -algebra, and A the carrier of the
algebra. For sake of simplicity, we will write A to denote the -algebra when
F and FA are non-ambiguous.
A substitution  assigns terms of appropriate sorts to variables. The domain
of  is dened by: xg. If t is a term, then t denotes
the application of  to t. If  applies every variable to a ground term, then
is a ground substitution. We denote by  the syntactic equivalence between
objects. Let N  be the set of sequences of positive integers. For any term
t, P os(t)  N  denotes its set of positions and the expression t=u denotes
the subterm of t at a position u. We write t[s] u (resp. t[s] ) to indicate that
s is a subterm of t at position u (resp. at some position).The top position
is written ". Let t(u) denote the symbol of t at position u. A position u in
a term t is said to be a strict position if position u in
a term t such that is a linear variable position if x
occurs only once in t, otherwise, u is a non linear variable position. A linear
variable of a term t is a variable that occurs only once in t. The depth of a
term t is dened as follows: is a constant or a variable, otherwise,
We denote by  a transitive irre
exive relation
on the set of terms, that is monotonic (s  t implies w[s] u  w[t] u ), stable
per instantiation (s  t implies s  t) and satises the subterm property
(f(   ; t;    )  t). Note that these conditions imply that  is noetherian.
The multiset extension of  will be denoted by . An equation is a formula
of the form l = r. A conditional equation is a formula of the following form:
It will be written V n
called a
conditional rule if flg  fr; a for each substitution .
The precondition of rule V n
. The term l is the
left-hand side of the rule. A rewrite rule c ) l ! r is left-linear if l is linear.
A set of conditional rules is called a rewrite system. A constructor is free if
it is not the root of a left-hand side of a rule. Let t be a term in T (C; X), t
is called a constructor term. A rewrite system R is left-linear if every rule in
R is left-linear. We dene jRj as the maximal depth of the strict positions in
its left-hand sides. Let R be a set of conditional rules. Let t be a term and u
a position in t. We write: t[l] u !R t[r] u if there is a substitution  and a
conditional rule V n
r in R such
for all i 2 [1    n] there exists c i such that a i  !
R c i .
Rewriting is extended to literals and clauses as expected.
A term t is irreducible (or in normal form) if there is no term s such that
t !R s. A term t is ground reducible i all its ground instances are reducible. A
completely dened if all ground terms with root f are reducible
to terms in T (C). We say that R is su-ciently complete if all symbols in D
are completely dened. A clause C is an expression of the
. The clause C is a Horn clause if m  1. The clause C is
positive if clause is a tautology if either it contains some subclause
or or some positive literal s. The clause C is a logical
consequence of E if C is valid in any model of E, denoted by E
say that C is inductively valid in E and denote it by E
ground substitution , (for all (there exists j,
We say that two terms s and t are joinable, denoted by
R v and t !
R v for some term v. The rewrite system R is
ground convergent if the terms u and v are joinable whenever
R
5 Observational semantics
The notion of observation technique (see e.g. [4]) has been introduced as a
mean for describing what is observed in a given algebra. Various observation
techniques have been proposed in the literature: observations based on sorts
[36,31,28,16], on operators [1], on terms [34,15,5] or on formulas [33,34,22]. An
observational specication is then obtained by adding an observation technique
to a standard algebraic specication.
Our observation technique is based on sorts but can easily be extended to
operators. Our observational semantics is based on a weakening of the satisfaction
relation. Informally speaking, behavioural properties of a data type
are obtained by forgetting unnecessary information. Then, objects which can
not be distinguished by experiments are considered as observationally equal.
5.1 Contexts
In the framework of algebraic specications, such experiments can be formally
represented by contexts of observable sorts and operators over the signature
of the specication. Thus, for showing that a certain property is valid for all
observable experiments, we formally reason about all contexts of observable
sorts and operators. The notion of context we use is close to the one used by
Bidoit and Hennicker [6].
Denition 5.1 (context) Let T (F; X) be a term algebra and
signature.
(1) a context over  (or -context) is a non-ground term c 2 T
distinguished linear variable called the context variable of c. To indicate
the context variable occuring in c, we often write c[z s ] instead of c, where
s is the sort of z s . A variable z s of sort s is a context called empty context
of sort s.
(2) the application of a context c[z s ] to a term t 2 T (F; X) of sort s is denoted
by c[t] and is dened as the result of the replacement of z s by t in c[z s ].
The context c is said to be applicable to t. The application of a context
to an equation a = b is the equation
(3) by exception, var(c) will denote the set of variables occuring in c but the
context variable of c. A context c is ground if
(4) a subcontext (resp. strict subcontext) of c is a context which is a subterm
strict subterm) of c with the same context variable.
The next lemma gives some properties about contexts.
Lemma 5.2 Let c[z s ] and c 0 [z 0
be two contexts such that c 0 is of sort s, t
be a term of sort s 0 and  be a substitution such that z s 62 dom(). Then
The notion of context is generalized to clauses. A clausal context for a clause
is a list of contexts which are to be applied in order to each equation (negated
or not) in the clause. The set of contextual variables of a clausal context is
the set of contextual variables of its components.
Denition 5.3 (clausal context) Let S be a set of contexts, then c is a
clausal context w.r.t. S for a clause
list of
contexts such that for i
applicable to e i . The application of c to C is denoted by c[C] and is equal to
the clause V m
We dene the composition of clausal contexts in the same way than for contexts

Denition 5.4 Let
n i be two clausal contexts
such that for i 2 [1::n] c i is applicable to c 0
. Then the composition of c
and c 0 denoted by c[c 0 ] is the clausal context fc 1 [c 0
]g.
Clausal contexts induce an ordering relation on clauses that we call context
subsumption since it is an extension of the classical subsumption ordering. It
can be viewed as a generalization of the functional subsumption rule dened
in [32] and is useful for redundancy elimination in rst-order theorem-proving.
Denition 5.5 (context subsumption) The clause C  )  contextually
subsumes C 0 if there exists a clausal context c and a substitution  such
that C 0  ) c[].
Note that the strict part of this ordering is well-founded by the same argument
than for standard subsumption. The lemma 5.2 can be extended to clausal
contexts in a straightforward way.
Lemma 5.6 Let c and c 0 be two clausal contexts, let C be a clause and  be
a substitution such that the contextual variables of c are not in dom(). Then
5.2 Observational validity
The notion of observational validity is based on the idea that two objects
in a given algebra are observationally equal if they cannot be distinguished
by computations with observable results. Computations are formalized with
contexts. For dening observational specications we need only to specify the
observable sorts. The notion of observational specication has been generalized
both in BOBJ's hidden logic [12] and CafeOBJ's coherent hidden algebra
logic [26], as well as in Bidoit and Hennicker's observational logic [7], by also
allowing non-behavioral operations, and we expect our results to generalize
directly to the general framework.
Denition 5.7 (observational specication) An observational specica-
tion SP obs is a quadruple (S; F; E; S obs ) such that (S; F ) is a signature, E is
a set of conditional equations, S obs  S is the set of observable sorts.
In the following we assume that an observational specication SP
obs ) is given with signature
specication: STACK
sorts: nat, stack
observable sorts: nat
constructors:
0: !nat;
s: nat !nat;
Nil: !stack;
nat  stack !stack;
dened functions:
pop: stack ! stack;
axioms:
top(push(i,s))=i
pop(Nil)=Nil
pop(push(i,s))=s
Fig. 1. Stack specication
Example 5.8 The specication Stack in Figure 1 is an observational speci-
cation where S fnatg.
Denition 5.9 An observable context is a context whose sort belongs to S obs .
An observable clausal context is a clausal context whose all component contexts
are observable. The set of observable contexts is denoted by C obs . For sake of
simplicity it will also denote the set of observable clausal contexts.
Example 5.10 Consider the specication stack in Figure 1. They are innite-
ly many observable contexts: top(z stack ); top(pop(z stack
Denition 5.11 The terms a; b are observationally equal if for all c 2 C obs
We denote it by E or simply a = obs b.
Example 5.12 Consider the stack specication in Figure 1. The equation
s is not satised in the initial algebra. However intuitively
it is observationally satised when we just observe the elements occurring
in push(top(s); pop(s)) and s. This can be proved formally by considering
all observable contexts.
Lemma 5.13 The relation = obs is a congruence on T
PROOF. The relation = obs is obviously an equivalence relation on T
for all us prove that f(a It is
su-cient to show by induction on j that
For immediately
us show that f(a
We consider an arbitrary observable context c[z] of sort s. Then
by induction hypothesis. We deduce:
Since a
are observable context we have:
By transitivity of = ind we have: c[f(a
)]. The induction step is then completed. 2
Our main goal is to generalize implicit induction proofs to an observational
framework. In particular if all sorts are observable the theory we obtain reduces
to a standard initial one. However this generalization of initial semantics is not
straightforward since our specications admit conditional axioms. For instance
let be two ground equations and assume that E 6j= ind
We may have E v. In this
case v. For this reason we
adopt a semantics that is close to the one dened by P. Padawitz [29].
Denition 5.14 (observational property) Let C  V n
. We say that C is an observational property (or observationally
valid) and we denote it by E
for all ground substitutions ,
(for all
such that E
obs is a congruence on T E) the quotient algebra
of T with respect to = obs . Some properties of T (F; E) are studied in [29].
In particular it is shown that T (F; E) is nal in the class of term-generated
and visibly initial algebras. The proof system that we develop in the following
sections is dedicated to the derivation of validity in the algebra T (F; E).
Theorem 5.15 Let C
E)
PROOF. This is a simple consequence of the fact that T (F; E)
6 Induction schemes
Our purpose in this section is to introduce the ingredients allowing us to
prove and disprove observational properties. This task amounts in general
to check an innite number of ground formulas for validity, since an innite
number of instances and an innite number of contexts have to be considered
for building these ground instances. This is where induction comes into play.
Test substitutions will provide us with induction schemes for substitutions
and critical contexts will provide us with induction schemes for contexts. In
general, it is not possible to consider all the observable contexts. However,
cover contexts are su-cient to prove observational theorems by reasoning on
the ground irreducible observable contexts rather than on the whole set of
observable contexts. In the following, we denote by R a conditional rewriting
system.
Denition 6.1 (cover set) A cover set, denoted by CS, for R, is a nite
set of irreducible terms such that for all ground irreducible term s, there exist
a term t in CS and a ground substitution  such that t  s.
We now introduce the notion of cover context that is used to schematize all
contexts. Note that a cover context need not be observable, (unlike crucial
contexts of [6]). The intuitive idea is to use cover context to extend the conjectures
by the top in order to create redexes. Then the obtained formulas can
be simplied by axioms and induction hypothesis.
Denition 6.2 (cover context set) A cover context set CC is a minimal
(for inclusion) set of contexts such that: for each ground irreducible context
c obs [z s substitution  such that
var(c) and c is a subcontext of c obs .
A cover context set for the specication stack is fz nat ; top(z stack ); pop(z stack )g.
The context push(i; z stack ) cannot belong to a cover context set since
z stack )) and pop(push(i; z stack are reducible. Note that
usually there are innitely many possible cover context sets. For
instance,fz nat ; top(z stack ); top(pop(z stack )); pop(pop(z stack ))g is also a cover context
set.
Similar notions called complete set of observers have been proposed by Hennicker
[17]. More recently another close concept has been introduced by
Goguen et al. [12].
Cover sets and cover context sets are fundamental for the correctness of our
method. However, they cannot help us to disprove the non observationally
valid clauses. For this purpose, we introduce a new notion of critical context
sets and we use test sets as dened in [8]. In the following, we rene cover
context sets so that not only we can prove behavioural properties but we
can also disprove the non valid ones. We need rst to introduce the following
notions:
A context c is quasi ground reducible if for all ground substitution  such that
A term t is strongly irreducible if none of its non-variable subterms matches a
left-hand side of a rule in R. A positive clause C pos  W n
strongly
irreducible if C pos is not a tautology and the maximal elements of fa
w.r.t.  are strongly irreducible by R.
An induction position of f 2 F is a position p such that there exists in R a
rewrite rule of left-hand side f(t is the position in f(t
of a function symbol or of a non-linear-variable subterm. Given R, the set of
induction variables of a term t, is the subset of variables of t whose elements
occur in a subterm of t of the form f(s
term for each i 2 [1::n], at an induction position of f . The notion of induction
variables is extended to clauses as expected.
Test sets and test substitutions are dened simultaneously.
Denition 6.3 (test set, test substitution) A test set is a cover set
which has the following additional properties: (i) the instance of a ground
reducible term by a test substitution matches a left-hand side of R. (ii) if the
instance of a positive clause C pos by a test substitution  is strongly irreducible,
then C pos  is not inductively valid w.r.t. R. A test substitution for a clause
C instanciates all induction variables of C by terms taken from a given test
set whose variables are renamed.
The following denition introduces our notions of critical context set and
critical clausal context.
Denition 6.4 (critical context set, critical clausal context) A critical
context set S is a cover context set such that for each positive clause
C pos , if c[C pos ] is strongly irreducible where  is a test substitution of C pos
and c is a clausal context of C pos w.r.t. S, then C pos  is not observationally
valid w.r.t. R.
A critical clausal context w.r.t. S for a clause C is a clausal context for C
whose contexts belongs to S.
Example 6.5 In Example 1 a set of critical contexts of R is:
fpop(z stack ); z nat ; top(z stack )g.
Test substitutions and critical context sets permit us to refute false conjectures
by constructing a counterexample.
Denition 6.6 (provably inconsistent) We say that the clause V n
j is provably inconsistent if and only if there exists a test
substitution  and a clausal critical context c such that:
(1) for all i, a i is an inductive theorem w.r.t. R.
strongly irreducible by R.
Provably inconsistent clauses are not observationally valid.
Theorem 6.7 Let R be a ground convergent rewrite system. Let C be a provably
inconsistent clause. Then C is not observationally valid.
PROOF. Let C  V n
j be a provably inconsistent
clause. Then there exists a critical context c and a test substitution  such
(i) for all i, R
strongly irreducible by R.
By Denition 6.4,
j ) is not observationally val<id w.r.t. R. Then
R 6j= Obs C by using (i). 2
Example 6.8 Consider the stack specication in Figure 1 and let us check
whether the conjecture observationally valid.
We apply rst an induction step, then we obtain:
1.
2.
Theses subgoals can be simplied by R, we obtain:
3.
4.
The equation We apply an induction step to
then we obtain:
5. top(nil)=x
6. top(push(y,z))=x
The equation simplied by R into which is provably
inconsistent. Now, since R is ground convergent, we conclude that
is not observationally valid.
6.1 Computation of test sets
The computation of test sets and test substitutions for conditional specica-
tions is decidable if the axioms are su-ciently complete and the constructors
are specied by a set of unconditional equations (see [23,21]). Unfortunately,
no algorithm exists for the general case of conditional specications. However,
in [8], a procedure is described for computing test sets when the axioms are
su-ciently complete over an arbitrary specication of constructors.
6.2 Computation of critical contexts
Let us rst introduce the following lemma which gives us a useful characterization
of critical context sets:
Lemma 6.9 Let R be a left-linear conditional rewriting system. Let CC be
a cover context set that such that for each context c[z s the variables
of c[z s ] appear at depth greater than or equal to jRj 1, and there exists an
observable context c obs such that c obs [c] is strongly irreducible. Then, CC is a
critical context set for R.
PROOF. Let C be a positive clause such that c[C] is strongly irreducible,
where  is a test substitution of C and c is a critical clausal context of C. Let us
prove that C is not observationally valid. If c 2 C obs , then, by Denition 6.3,
we conclude that c[C] is not an inductive theorem, and therefore C is not
observationally valid. Assume now that c 62 C obs . By assumption, there exists
c is not quasi ground
reducible, and does not contain any observable strict subcontextg
c is not quasi ground reducible,
c does not contain any observable subcontext, and all variables (including the
context one) in c occur at jRj g.
repeat
[c] is not quasi ground reducibleg
until CC
output: CC i
Fig. 2. Computation of Critical Contexts
an observable clausal context c obs such that c obs [c] is strongly irreducible. Let
us show that c obs [c[C]] is strongly irreducible. Assume otherwise that there
exists a rule with left-hand side l that applies to c obs [c[C]] at a position p. For
every nonvariable position p 0 of l, pp 0 is a nonvariable position of c obs [c] since
the variables of c[z s ] appear at depth greater than or equal to jRj 1. Since l is
linear, we can dene a substitution  such that for every variable x that occurs
at position q of l we have x  c obs [c]=pq. We then have c obs [c]=p  l, which
contradicts the assumption that c obs [c] is strongly irreducible. So c obs [c[C]]
is strongly irreducible. Then, by Denition 6.3, c obs [c[C]] is not inductively
valid. Thus, R 6j= Obs C. 2
us present our method for constructing such critical contexts. The
idea of our procedure is the following: starting from the non quasi ground reducible
observable contexts of depth smaller than or equal to jRj, we construct
all contexts that can be embedded in one of those observable contexts to give
a non quasi ground reducible and observable context.
The quasi ground reducibility is co-semidecidable for conditional rewrite systems
by the same argument that has been employed for ground reducibility
[20]. The procedure amounts to enumerate all the ground instances of a term
and to check them for reducibility. It can be proved by reduction to ground
reducibility that quasi ground reducibility is decidable too for equational systems

Proposition 6.10 Given a set of non conditional rewrite rules R and a context
c[z s ], it is decidable whether c[z s ] is quasi ground reducible.
PROOF. Let us rst introduce a new constant symbol d 62 F . Let Red l (x)
be a unary predicate on T which is true if the ground term x contains a
subterm that is an instance of l. The context c[z s ] is quasi ground reducible i
all instances of c[d] by substitutions  satisfying 8x x 2 T are reducible
by R. We denote by G the set of ground terms in T that contain one
and only one occurrence of d. Note that G is a regular tree language. Hence the
quasi ground reducibility of c[z s ] can be expressed by the rst-order formula:
Red
_
Red l i
where the set of left-hand sides of R is g. Such formula can be
decided thanks to Theorem 4.18 of Caron et al. [10]. 2
The following proposition is also useful for testing that a context is quasi
ground reducible.
Proposition 6.11 Let R be an equational rewriting system such that all dened
functions are completely dened over free constructors. Given a context
of the form f(t is a completely dened function and for
is a constructor term. If z s does not appear at an induction
position of f then c[z s ] is quasi ground reducible.
PROOF. Assume that there exists a ground instance of c[z s ] of the form
which is irreducible by R. Consider the substitution   z s s
where s is a ground and irreducible constructor term. Then f(t
ground and irreducible. Assume otherwise that there exists a rule with left-hand
side l that applies to f(t be the position of z s in c[z s ].
Then, at the position p appear a function symbol in l and therefore p is an
induction position of f , in contradiction with the assumption that p is not
an induction position of f . So, f(t ground and irreducible. This
contradicts the assumption that f is completely dened. 2
Theorem 6.12 Let R be a rewriting system and CC be the result of the
application of the procedure given in Figure 2. Then:
(1) CC is a cover context set for R.
(2) if R is equational and left-linear then CC is a critical context set for R.
PROOF. It is relatively easy to show that CC is a cover context set for
R. Now, assume that R is equational and left-linear and let us prove that
CC is also a critical context set for R. By construction, any non-observable
context in CC has variables at depth greater than or equal to jRj. Now,
since R is equational, any non quasi ground reducible context is necessarily
strongly irreducible. On the other hand, R is left-linear and the variables of
non-observable context occur at jRj, then for each context c[z s
exists i such that c 2 CC i , we can show that there exists an observable context
c obs such that c obs [c] is strongly irreducible. The proof is done by induction on
specication: LIST
sorts: nat, bool, list
observable sorts: nat, bool
constructors:
0: !nat;
s: nat !nat;
Nil: !list;
insert: nat  list !list;
True: !bool;
False: !bool;
dened functions:
union: list  list ! list;
in: nat  list ! bool;
eq: nat  nat ! bool;
axioms:
union(Nil,l)=l
in(x,Nil)=False
eq(x,y)=True
eq(x,y)=False
eq(0,0)=True
eq(0,s(x))=False
eq(s(x),0)=False
Fig. 3. List specication
Example 6.13 Consider the Stack specication in Figure 1. We have
stack ); push(i; z stack )g.
critical context set for R.
Example 6.14 Consider the List specication in Figure 3. We have:
list )g,
list ; x); insert(x; z list )g,
list ; x)g.
is a cover context set for R. In fact, union(x; z list ) is quasi
ground reducible and in(y; union(z list ; x)) is not quasi ground reducible since
list ; N il)) is irreducible, but in(y; insert(x; z list )) is quasi ground
reducible.
It is possible to compute critical context sets in the case where R is a conditional
rewriting system. It is su-cient to apply our procedure given in Figure 2
to compute a cover context set CC, and then to check that for each non observable
context c 2 CC, there exists an observable context c obs such that c obs [c] is
strongly irreducible. In Example 6.14, we have in(x; (union(z list ; y) is strongly
irreducible, then we conclude that list ); union(z list ; x)g
is a critical context set for R.
7 Inference system
The inference system we use (see Figure 4) is based on a set of transition
rules applied to is the set of conjectures to prove and H
is the set of induction hypotheses. The initial set of conditional rules R is
oriented with a well founded ordering. An I-derivation is a sequence of states:
We say that an I-derivation is fair if
the set of persistent clauses ([ i \ ji
Context induction is performed implicitly by the Generation rule. A clause
is extended by critical contexts and test sets. These extensions are simplied
either by Deletion or by Contextual Simplification or by Case
Simplification. The resulting conjectures are collected in S
Simplification illustrates the case reasoning: it simplies a conjecture with
conditional rules.
Contextual Simplification can be viewed as a powerful generalization of
contextual rewriting [38] to allows to simplify observational properties. The
rule Context Subsumption appeared to be very useful for manipulating
non orientable conjectures.
An I-derivation fails when there exists a conjecture such that no rule can be
applied to it. An I-derivation succeeds if all conjectures are proved.
Example 7.1 Let us take the signature and the axioms of the specication in

Figure

1 and let us add a new function elem : nat ! bool and the following
axioms:
Assume that the observable sort is bool. A test set here is
and a critical context is
)g.
We can easily show that top(y) is not an inductive theorem but it is
observationally valid, since for all ground term t, top(t) reduces either to 0 or
to s(0), and
Note that in this example, we have relations between constructors and that it
cannot be handled by the other related approaches [12,26].
Theorem 7.2 (correctness of successful I-derivations) Let
be a fair I-derivation. If it succeeds then R
PROOF. Suppose R 6j= obs E 0 and let M be the set of minimal elements
w.r.t.  of fC j is a ground irreducible substitution, such that
R 6j= obs Cg. Note that M 6= ; since R 6j= obs E 0 and  is well founded.
Let C 0 be a clause in M such that C 0 is minimal w.r.t context subsumption.
Then there exist a clause and an irreducible ground substitution
such that C We have R 6j= obs C, then we can consider an observable
context c obs such that R 6j= c obs [C]. Without loss of generality we can assume
that c obs is irreducible: otherwise it can be simplied by R to an irreducible
one with the same property. Now, we show that no rule can be applied to C.
This shows that the derivation fails since C must not persist in the derivation
by the fairness hypothesis.
Hence let us assume that C
rule applied to C. We discuss now the situation according to which rule is
applied. In every case we shall derive a contradiction. In order to simplify the
notations we write E for E j and H for H j .
Case Simplification: suppose that the rule Case Simplification is
applied to C. Since R . Then, there exists k such that
R
have R 6j= c obs C[l], R . Then R 6j= Obs C k .
On the other hand, C Contradiction, since we
have proved the existence of an instance of a clause of [ which is not
observationally valid and which is smaller than C.
Contextual Simplification: suppose that the rule Contextual Simplification
is applied to C. Without loss of generality, we can assume
that C   )
the context built from s by replacing l by the context variable z and let
c obs  c 1::n+1
obs
obs i. We have:
and C is a minimal counterexample,
then R
obs [].
Hence, R
obs [c s [r]]. So, we conclude that
On the other hand, C
Generation: Suppose that the rule Generation is applied to C. Since the
substitution  is ground and irreducible, there exists a ground substitution
and a test substitution  such that  = . Besides, since R 6j= Obs C,
then we can consider an irreducible ground observable context c obs such that
R 6j= c obs [C]. Since c obs is ground and irreducible, then there exists a critical
context c and c 0 2 C obs such that c
If Deletion is applied, then R
If Contextual Simplification or Case Simplification is applied to
c[C], then by following the same reasoning used in the proofs of soundness
of Contextual Simplification and Case Simplification we derive a
contradiction.
Context Subsumption: Since R 6j= Obs C, C cannot be contextually
subsumed by an axiom of R. If there exists C fCg) such that
we have R 6j= c[C 0 ], then, c is an empty context,
and since C is minimum in [ subsumption ordering.
Therefore, C 0 62 (E n fCg). On the other hand C 0 62 H, otherwise the rule
Generation can also be applied to C, in contradiction with a previous case.
Hence this rule cannot be applied to C.
Deletion: Since R 6j= Obs C, C is not a tautology and this rule need not be
considered.Theorem 7.3 (correctness of disproof) Let
an I-derivation. If there exists j such that Disproof is applied to
then R 6j=
PROOF. If there exists j such that Disproof is applied to
by Theorem 6.7, we conclude that R 6j= . Now, to prove that R 6j=
it is su-cient to prove the following claim: Let
an I-derivation step. If 8i  j; R
by a simplication rule, then the equations which are used for
simplication occur in some and therefore are observationally
valid in R by assumption. Hence, E j+1 is observationally valid too in R. If
by Generation on C every auxiliary equation
which is used for rewriting an instance of C by a critical context c and a test
substitution , is either in R or observationally
valid in R. If Subsumption or
Deletion, then E j+1  E j and therefore E j+1 is observationally valid in R. 2
Now we consider boolean specications. To be more specic, we assume there
exists a sort bool with two free constructors ftrue; falseg. Every rule in R is
of type: V n
Conjectures will be boolean clauses, i.e. clauses whose negative literals are of
completely dened
symbol in R. Then f is strongly complete [8] w.r.t R if for all the rules
whose left-hand sides are identical up to a renaming  i , we
have R
We say that R is strongly complete if for all f 2 D, f
is strongly complete w.r.t R.
Theorem 7.4 (refutational completeness) Let R be a conditional rewrite
system. Assume that R is ground convergent and strongly complete. Let E 0 be
a set of boolean clauses. Then R 6j= derivations issued from
Case Simplication:
if R
Contextual Simplication:
or A  C)
where A
Context Subsumption:
contextually subsumes C
Deletion:
if C is a tautology
Generation:
if for all critical context c and test substitution :
where
" is the application of Deletion, or Contextual or Case Simplication
Disproof
if C is provably inconsistent
Fig. 4. Inference System I
PROOF. by Theorem 7.2. (: The only rule that permits us to introduce
negative clauses is Case Simplification. Since the axioms have boolean
preconditions and E 0 only contains boolean clauses, all the clauses generated
in an I-derivation are boolean. If Disproof is applied in an I-derivation, then
there exists a positive clause C such that Generation cannot be applied to
C. Therefore there exists a critical context c and a test substitution  such that
R 6j= c[C]. Moreover c[C] does not match any left-hand side of R. Otherwise,
the Contextual Simplification rule or the Case Simplification rule
can be applied to c[C] since R is strongly complete. As a consequence, C is
a provably inconsistent clause and therefore R 6j=
8 Computer experiments
Our prototype is written in Objective Caml on top of Spike. It is designed
to prove and disprove behavioural properties in conditional theories. The nice
feature of our approach is that it has needed only a few modications of the
implicit induction system Spike to get an operational procedure for observational
deduction. Also most optimisation and strategies available with Spike
can also be applied to the observational proof system.
The rst step in a proof session is to compute test sets and critical contexts.
The second step is to check the ground convergence of the set of axioms. If
these steps succeed we can refute false behavioural properties. If the computation
fails the user can introduce his own cover sets and cover contexts. After
these preliminary tasks the proof starts.
Example 8.1 We proved automatically that push(top(S);
behavioural property of the stack specication (see Figure 1). Note that this
example fails with the approach of [6], since it is not possible to compute automatically
a set of crucial contexts: if two stacks have the same top they are not
necessarily equal. In the approach of [16], we have to introduce an auxiliary
function iterated pop : nat  stack ! stack such that iterated pop(n; s) iterates
times pop. This is easy because pop is unary. The function iterated pop
is dened by:
iterated pop(0; iterated pop(n; pop(s))
Then, we have to prove the property for all contexts of the form
top(iterated pop(x; c[z stack ])). However, this schematization of contexts could
be more complicated in case of a function of arity greater than two. So, this
process seems to be not easy to automatize in general. In the approach of [25],
this problem remains too.
us describe our proof. The prover computes rst a test set for R and
the induction positions of functions, which are necessary for inductive proofs.
It also computes a critical context. These computation are done only once and
before the beginning of the proof.
test set of R:
critical contexts of R:
induction positions of functions:
Application of generation on:
it is subsumed Nil of R
Delete
it is subsumed
it is subsumed
Delete
it is subsumed
The initial conjectures are observationally valid in R
Example 8.2 Consider now the specication list in Figure 3. The theorem
automatically proved.
test set of R:
list
critical contexts of R:
induction positions of functions:
Application of generation on:
Delete
Delete
it is subsumed True of R
Simplification of:
Simplification of:
Delete
Application of generation on:
Delete
Delete
Delete
it is subsumed True of R
Simplification of:
False by R:
Delete
it is subsumed True of H4
The initial conjectures are observationally valid in R
In the same way we have proved the following conjectures:
9 Conclusion
We have presented an automatic procedure for proving observational properties
in conditional specications. The method relies on the construction of a
set of critical contexts which enables to prove or disprove conjectures. Under
reasonable hypotheses, we have shown that the procedure is refutational com-
plete: each non observationally valid conjecture will be detected after a nite
time.
We have shown the potential of our context induction technique for reasoning
about object behaviours and especially for renement. With our implementation
we proved several examples in a completely automatic way.
A cover context w.r.t. our denition 6.2 garantees the soundness of our proce-
dure. However, cover contexts computed by our procedure may contain unecessary
contexts, as in Example 3 where union(z list ; x) is useless for observations.
We plan to rene our notion of cover and critical contexts in order to select
only the needed contexts. We also plan to extend the observation technique
to terms and formulas. In the near future we plan to extend our approach to
verify properties of concurrent and distributed object systems.

Acknowledgements

We thank Diane Bahrami and the referees for their helpful
comments.



--R

Proving the correctness of algebraically speci
Observational Proofs with Critical Contexts.
Proving the correctness of algebraic implementations by the ISAR system.
Behavioural approaches to algebraic speci
Towards an adequate notion of observation.
How to prove observational theorems with LP.
Behavioural theories and the proof of behavioural properties.
Automated theorem proving by test set induction.
Implicit induction in conditional theories.
Encompassment properties and automata with constraints.
Fundamentals of Algebraic Speci
Rosu and K.
Towards an algebraic semantics for the object paradigm.
The speci
Implementation of parameterized observational speci
Context induction: a proof principle for behavioural abstractions and algebraic implementations.
Structured speci

Reasoning about Classes in Object-Oriented Languages: Logical Models and Tools
On the decidability of quasi-reducibility
Automating inductionless induction using test sets.

Testing for the ground (co-)reducibility property in term-rewriting systems
Extending Bachmair's method for proof by consistency to the
Proving correctness of re
Test Towards Automated Veri cation of Behavioural Properties
Verifying Behavioural Speci
Initial behaviour semantics for algebraic speci
Computing in Horn Clause Theories.
Proofs in the
Behavioural validity of conditional equations.

On observational equivalence and algebraic speci
Toward formal development of programs from algebraic speci
Towards formal development of ml programs: foundations and methodology.
Final algebra semantics and data type extensions.
Algebraic speci
Implementing Contextual Rewriting.
--TR
On observational equivalence and algebraic specification
Toward formal development of programs from algebraic specifications: implementations revisited
Computing in Horn clause theories
Initial behavior semantics for algebraic specifications
Theorem-proving with resolution and superposition
Automating inductionless induction using test sets
Algebraic specification
Towards an adequate notion of observation
Testing for the ground (co-)reducibility property in term-rewriting systems
Extending Bachmair''s method for proof by consistency to the final algebra
Behavioural approaches to algebraic specifications
Towards an algebraic semantics for the object paradigm
Behavioural theories and the proof of behavioural properties
Automated theorem proving by test set induction
Fundamentals of Algebraic Specification I
Reasonong about Classess in Object-Oriented Languages
Specifications with Observable Formulae and Observational Satisfaction Relation
Proving the Correctness of Algebraically Specified Software
Proving the Correctness of Algebraic Implementations by the ISAR System
How to Prove Observational Theorems with LP
Behaviour-Refinement of Coalgebraic Specifications with Coinductive Correctness Proofs
Implementation of Parameterized Observational Specifications
Toward Formal Development of ML Programs
Encompassment Properties and Automata with Constraints
Implementing Contextual Rewriting
Verifying Behavioural Specifications in CafeOBJ Environment
Circular Coinductive Rewriting
The specification and application to programming of abstract data types.

--CTR
Abdessamad Imine , Michal Rusinowitch , Grald Oster , Pascal Molli, Formal design and verification of operational transformation algorithms for copies convergence, Theoretical Computer Science, v.351 n.2, p.167-183, 21 February 2006
Grigore Rosu, On implementing behavioral rewriting, Proceedings of the 2002 ACM SIGPLAN workshop on Rule-based programming, p.43-52, October 05, 2002, Pittsburgh, Pennsylvania
Manuel A. Martins, Closure properties for the class of behavioral models, Theoretical Computer Science, v.379 n.1-2, p.53-83, June, 2007
rewriting;induction;automated proofs;observational semantics