Using Term Rewriting to Verify Software.
This paper describes a uniform approach to the automation of verification tasks associated with while statements, representation functions for abstract data types, generic program units, and abstract base classes. Program units are annotated with equations containing symbols defined by algebraic axioms. An operation's axioms are developed by using strategies that guarantee crucial properties such as convergence and sufficient completeness. Sets of axioms are developed by stepwise extensions that preserve these properties. Verifications are performed with the aid of a program that incorporates term rewriting, structural induction, and heuristics based on ideas used in the Boyer-Moore prover. The program provides valuable mechanical assistance: managing inductive arguments and providing hints for necessary lemmas, without which formal proofs would be impossible. The successes and limitations of our approaches are illustrated with examples from each domain.
Introduction
Many different methods have been used to annotate software and prove properties about it. Fewer
attempts have been made to adapt a single notation to a variety of different annotation tasks and
explore the interactions between the types of tasks, properties of the specifications, and demands of
verification techniques. In this paper, we apply equational specification and reasoning techniques
to verify properties of while statements, abstract data types, generic program units, and derived
classes. We present new techniques for computing the weakest preconditions of while statements,
annotating abstract base classes from which other classes are derived, and designing algebraic specifications
which are convergent and sufficiently complete. In addition, we discuss an experimental
tool for partially automating verification activities and report some of our experiences using these
techniques and tool.
This research has been supported in part by the National Science Foundation grant CCR-8908565 and the Office
of Naval Research grants N00014-87-K-0307 and N0014-90-J4091.
Rewriting [10, 26] is central to our approach. We use rewriting concepts both for designing small
specifications with desirable properties, such as completeness and consistency, and for extending
specifications incrementally while preserving these properties. We also use rewriting concepts for
proving that programs are correct with respect to their specifications.
Abstraction and factorization reduce the amount of detail that needs to be considered when
solving problems. Specifications play a key role in abstraction, hiding details of implementations,
and in factoring program components, collecting program units with common semantics rather
than just common syntax.
The weakest precondition [11] of a while statement abstracts the particular state transformation
induced by a while statement to a class of state transformations which satisfy a particular post-condition
[17]. The notion of weakest precondition extends the method proposed in [20] to include
termination. Since both termination and verification of programs are unsolvable, it is somewhat
surprising that one can compute a first order expression of the weakest precondition of a while statement
[8, 32]. This expression, however, involves concepts such as G-odelization or Turing machines,
which cannot be reasoned about automatically. We introduce a notation called power functions
to describe while statements' state transformations. Power functions are described with algebraic
equations, as are the operations which appear in while statements' postconditions. Thus, we may
reason about power functions in the same automated way we reason about the operations appearing
in program annotations. Power functions also allow us to address incompleteness problems arising
in the verification of while statements involving abstract data types [24, 30].
Abstract data types permit program proofs to be factored into two parts: proofs of programs
which depend only on abstract properties of objects, and proofs that implementations of types
guarantee the abstract properties. In the second type of proof, implementations manipulating concrete
objects must satisfy pre and postconditions containing abstract objects. Hoare [21] introduced
representation mappings to map concrete objects to their corresponding abstract objects to make
such reasoning possible. We show that representation mappings can be cast within the equational
framework, allowing us to reap the benefits of equational reasoning and automated term rewriting.
Parameterized subprograms factor similar operations on different objects with the same types,
thus reducing the sizes of programs. Generic clauses, like those in Ada, extend the benefits of
factoring to program units which manipulate objects with different types. Generic formal type parameters
represent classes of types providing a few basic operations (e.g., assignment or equality).
Additional generic formal subprogram parameters can be specified to access additional operations.
When a generic unit is instantiated, only syntactic discrepancies are reported between the types
of the formal and actual generic subprogram parameters. Alphard's designers [31] were among the
first to suggest that functions defined with generic type parameters have semantic restrictions that
guarantee the functions are properly instantiated. Several research projects are currently investigating
how such restrictions should be stated and checked [13, 14, 16]. We use equational reasoning
to show that formal parameter specifications denoting properties required of actual parameters are
checked when generic program components are instantiated.
Object-oriented programming languages permit new classes to be defined via inheritance. A
superclass defines interfaces (and perhaps implementations) for operations, which are inherited by
its subclasses. In order to factor the implementation of a common operation in a superclass, each
subclass that redefines operations used in implementations of common operations must ensure that
its new operations have behaviors which are consistent with those of the respective superclass's
operations. That is, each subclass must behave like a subtype of the supertype. Groups of researchers
3[1, 28, 29] are currently defining subtype relations. We present a method for annotating
abstract base classes and other classes which are derived from them. Using equational reason-
ing, we show that derived classes are subtypes of an abstract base class in a manner similar to that
in [19].
In Section 2, we discuss these four classes of verification problems. Although we limit the
size of our examples to dimensions suitable for a technical presentation, they are representative of
increasingly larger programming problems.
The common denominator for these verification tasks is that we use equations both to annotate
each of the program components and to reason about the annotations. In Section 3, we address
the problems of both the quality and the expressiveness of specifications on which annotations
are based. We motivate the need of structuring specifications as rewrite systems both to ensure
crucial properties of specifications and to overcome inherent difficulties of equational reasoning. We
present design strategies for extending a specification while preserving its properties as a rewrite
system.
In Section 4, we briefly describe an automated tool for formally proving the obligations arising
from verification problems. In Section 5, we discuss the use of this tool and informally compare its
performance with another automated prover. Section 6 contains our conclusions.
Annotation and Verification
2.1 While Statements
Power functions [2] are a device to express the weakest precondition of a while statement in a form
which is useful for stating and verifying program correctness. We briefly review this technique and
show its application in two examples. In a later section we show how to automate the steps of the
process.
For any statement w and postcondition R, the weakest precondition wp(w; R) of w with respect
to R describes the set of all states S such that when w is activated in a state s in S it terminates
in a state r satisfying R [11]. If w is a while statement with condition b and body stmt, then
(R) is defined recursively as follows:
If the while statement is not defined on some state s, then wp(w; R)(s) is false, since H k (R)(s) does
not hold for any k.
The power function of a function f , whose domain and range are identical, embodies the k-fold
composition of f . If [stmt] is the function computed by statement stmt and s is a state, the power
function pf of [stmt] is defined as
s; if
undefined, otherwise.
Every function has a unique power function; and the totality, computability, and primitive recursiveness
of a function imply similar properties for its power function [2].
Using the notion of power function, we can obtain a first order expression of the weakest
precondition of a while statement with respect to any first order postcondition. If [stmt] is a total
function and pf is its power function, then
The expression -i P (i) stands for the minimum non-negative integer i, if it exists, such that P (i)
holds. More precisely, the second conjunct of the right side is a short hand for :b(pf (k;
is the least value such that k applications of the [stmt] to the original
state produce a state in which b evaluates to false. This yields the following equation
The right side requires only pf , the power function of [stmt], which is immediately obtained via
equation (1).
Often, we find it convenient to express a power function in terms of other functions that capture
higher level abstractions. We show one such example below, where very loosely speaking we say
that the power function of a maximum accumulator is the maximum of a sequence. In this case
we must ensure the validity of our claim, i.e., we must prove that some function pf is the power
function of a given function f . We call this step validation of pf with respect to f .
The weakest precondition of a while statement is more manageable when in equation (2) the
conjunct can be solved with respect to k, i.e., the value of k can be explicitly
determined from s. We call this step minimization of the loop. Loop minimization is obviously an
unsolvable problem since it is more difficult to demonstrate than loop termination. In the following
examples we show how to minimize loops and how this operation considerably simplifies the weakest
precondition.
Example 1
Consider the following program with while statement w and postcondition R:
where max(a[1::n]) is the largest value in the set a[n]g.
The function computed by the while statement body ([stmt]) returns the program state after
examining one component of the array.
Its power function (pf ) returns the program state after examining a slice of the array.
where max(a[i::j]; m) is the largest value in the set mg. We use induction to validate
pf , i.e., to show that it is indeed the power function of [stmt].
Base
The minimization of the loop requires us to demonstrate that -k(i+k ? n) is Substituting
this expression for k, we can calculate wp(w; R).
Although the annotations appear to use familiar, "well-defined" functions such as addition and
max, we have actually overloaded the function symbol max. Assuming all the scalar values are
natural numbers, one version of max is defined on two naturals, another on an array of naturals,
and a third on an array of naturals and a natural. Algebraic axioms permit us to define the relations
between symbols that appear in specifications.
natarray \Theta nat \Theta nat ! nat
natarray \Theta nat \Theta nat \Theta nat ! nat
With these definitions, wp(w; R) can be expressed as:
The initializing statements i := 2; m := a[1] transform the above equation into
which can be verified for any a and n ? 0.
Each of the verification tasks outlined above can be expressed as equations and verified me-
chanically. These tasks are:
1. Power function validation
Base cases add(0;
Inductive cases add(k
2. Loop minimization
3. Loop initialization
Example 2
The previous example shows that one may need to define new symbols for the analysis of a loop.
This is not a peculiarity of our method. Classic approaches to correctness verification may fail due
to the lack of expressiveness of data type specifications [24, 30]. For example, Kamin shows that a
program containing the following while statement
cannot be properly annotated by the lack of expressiveness of the usual theory of type Stack. A
similar result appears in [30].
Equation (2) implies that all one needs to properly annotate a loop is the power function of (the
functional abstraction of) the loop body. Rather than using equation (1), we chose to formulate the
power function of the loop in terms of high-level abstractions. These abstractions capture formally
the intuitive concepts that allow a programmer to code the above program.
The repeated execution of the loop body has the effect of chopping off a topmost portion of s,
reversing it, and placing it on top of t. The concept of separating a sequence into an initial portion
and a remainder generalizes the usual head and tail operations on sequences. We associate the
symbols drop and take with the more general operations and axiomatize them below.
stack
newstack
stack
newstack
newstack
The operation drop is denoted pop   in [24] and is required to make the type stack expressive. drop is
the power function of pop. The operation take returns the portion of a stack dropped by drop. We
formulate the power function of the loop (pf ) from the functional abstraction of the body ([stmt]),
exactly as informally stated earlier.
pf (k; (s;
where concat and reverse are defined as usual.
stack \Theta stack ! stack
concat(push(s;
stack
newstack
To validate pf we prove that
The last equation is not an instance of the second case of equation (1). It stems from a simple
result [2, Th. 5.7] concerning the equivalence of two formulations of power functions, i.e., accumulation
vs. recursion.
To minimize the loop we define the operation size, which computes the size of a stack, axiomatize
isnewstack, and verify -k(isnewstack(take(k;
The minimization of the loop is obtained by proving that
The latter is equivalent to isnewstack(drop(size(s); s)). Substituting permits us to
calculate wp(w; R).
R(pf
Initializing t with newstack and s with s 0 results in the following wp for the program:
which holds for any s 0 .
2.2 Data Type Implementations
Modern programming languages provide special constructs to implement user-defined data types.
These constructs are specifically designed to hide the representation of a type from its users. Code-level
verification techniques, such as those discussed in Examples 1 and 2 are insufficient to address
the correctness of an implementation because of the wide gap between the low-level operations
performed by the code and the high-level operations described by the operation's interface. For
example, decrementing an integer variable may be all it takes to pop a stack. However, verifying that
the variable is decremented does not ensure that the code correctly implements the pop operation.
We need to show that the code fulfills its obligations to the abstract operations [21].
Example 3
An implementation of the data type stack may represent an instance of the type by a record as
follows:
subtype index is integer range 1::size;
type data is array (index) of item;
type stack is record
range 0::size := 0;
items
This code fragment belongs to a package with generic arguments size, a positive, and item, a
private type.
The correctness of an implementation of the type stack entails the type's representation mapping
[21]. This function, denoted with A below, maps a concrete instance of stack, represented by
the above record, to its abstract counterpart.
newstack; if
The implementation of the stack operation pop is straightforward.
procedure pop(q : in out stack) is
begin
then raise underflow ;
else q:pntr := q:pntr \Gamma
On input a stack q, pop raises an exception if q:pntr = 0, that is, q:pntr ? 0 is a precondition for the
normal termination of the procedure. If the precondition is satisfied, pop simply decrements q:pntr.
The implementation is correct if clients of the stack package, to which the stack representation and
the procedure code may be hidden, indeed perceive decrementing q:pntr as popping q.
The proof method proposed by Hoare reduces the correctness of the implementation to individual
obligations of each procedure of the package. Omitting for readability the qualification of pntr
and items, the obligation of the procedure pop is
Standard techniques [20] reduce the correctness of the code to the truth of
where "false" in the first disjunct describes the (impossible) initial state that would result in the
normal termination of the procedure pop when the exception underflow is raised. The representation
mapping can be defined equationally and the proof obligation can be discharged automatically using
the tool discussed in Section 4.
2.3 Instantiations of Generic Program Units
Modularity is an essential feature for the design and implementation of large programs. Generic
type and subprogram parameters have been added to statically typed programming languages to
avoid duplicating an operation's source code in cases where it manipulates objects only through
other operations that are either implicitly defined for its generic formal type parameters or appear as
generic formal subprogram parameters. Interconnection errors become more likely and more subtle
when such language features are used. Compilers and/or loaders verify only syntactic properties
of module interconnections. The verification of (semantic) correctness entails activities similar
to those required for the verification of loops and data types discussed earlier, i.e., axiomatizing
symbols used for asserting properties or requirements of modules, and proving theorems, expressed
by means of these symbols, about the modules.
Example 4
Many computations on sets or sequences of elements are instances of a general paradigm referred
to as accumulation [4], for example, finding the maximum element, computing the sum of the
elements, or counting how many elements have a certain property. These computations can be
implemented by a loop whose body processes a new element of the sequence on each iteration. A
special variable, whose initial value depends on the computation being performed, "accumulates"
the result of the computation for the portion of the sequence processed thus far.
Example 1 presented earlier is an instance of accumulation in which the sequence of elements
is represented by an array and the process being performed is finding the maximum. In a language
supporting generic parameters, the interface of a simple accumulator (in which the types of the
elements and the accumulated result are the same) appears as follows:
type
type vector is array(integer range !?) of elem;
with function step(a; b : elem) return elem;
return elem is
begin
for i in v 0 first last loop
a := step(a; v[i]);
return a;
When a generic subroutine is instantiated (e.g., with actual parameters natural, nat vect, 0, and
max, as shown below) discrepancies may be detected between the types of the generic subprogram
parameters and the types of the actual objects bound to them.
procedure main is
function max array is new
accumulator(elem
Unfortunately, only syntactic discrepancies are reported. Some implementations of an accumulator
may rely on semantic properties which do not hold for all bindings, but cannot be detected by the
compiler.
For example, certain accumulations can be performed in parallel. In the simplest form, a
parallel implementation of an accumulator may simultaneously activate two tasks. Each task is an
accumulator operating on half of the input array and feeding its results to the function step which
returns the desired value. To improve the implementation's efficiency, we can use a tree-like cascade
of tasks each executing a single invocation of step in parallel. However, the parallel implementation
of the accumulator assumes that the function bound to the generic parameter step is associative and
that the element bound to the parameter init is its left identity i.e., (elem; step; init) is a monoid.
This result can be established in the following manner. Let e 1 be the sequence of values
processed by the accumulator, and A the function defined by
With the techniques described in Section 2.1 we can prove that A is the function computed by the
code of accumulator. If for all k such that i - k - j, the following equation holds
we can implement our accumulator in parallel as described above. It is easy to show that equation
(3) holds when elem is a monoid.
Algebraic notation can be used to specify properties of generic subroutine parameters that can
be verified from the specifications of the actual parameters. Such restrictions can be made explicit
by writing them as conditions and including them with the text of the specification of accumulator.
step(step(x;
When the function accumulator is instantiated with actual arguments replacing the formal parame-
ters, the identifiers in the axioms of the actuals can be replaced by the names of the formals and the
specification of the actual arguments can be used to prove these conditions. For example, it is easy
to verify these conditions for the operation max 0 , the maximum of two natural numbers, specified
in Example 1. Likewise, the instantiation requirement holds for both addition and multiplication,
but not for exponentiation. Thus, exponentiation cannot be legally bound to the generic parameter
step.
2.4 Inheritance
Object-oriented programming languages permit the definition of new classes via inheritance. A
subclass inherits data representations and operations from a superclass and may add or redefine
these components. We use algebraic equations to specify both the behavior of classes and to verify
that a subclass relation is also a subtype relation.
Example 5
In the following example, Shape is an abstract class; it can serve as a superclass for another class
but no objects of type Shape may be created.
class Shape -
public:
virtual Point center () const -
return Point ((left()
virtual void move (const Point &
void recenter (const Point& p) - move (p-center()); -;
virtual double top
virtual double bottom
virtual double left
virtual double right
An abstract class is used to define interfaces for operations which manipulate objects created by
its subclasses. For example, recenter moves an object to a new position.
Circle is declared as a subclass of Shape, redefining the latter's center operation with a more
efficient version of its own and providing definitions for those operations which are pure virtual
functions in Shape (i.e., move, top, etc.
class Circle : public Shape -
public:
Circle (const Point & C, const double
inline void radius (const double & R) - assert (R?=0); -radius = R; -;
inline double radius () const - return -radius; -;
inline void center (const Point & C) -center = C; -;
inline Point center () const - return -center; -;
inline void move (const Point & P) -center.move(P); -;
double top () const - return (-center.y()
double bottom () const - return (-center.y() -radius); -;
double left () const - return (-center.x() -radius); -;
double right () const - return (-center.x()
private:
Point
double -radius;
When it is passed a reference to a Circle object, recenter invokes Circle's center and move
operations.
Point p1(10,10), p2(5,5);
Circle c(p1,20);
We can use algebraic specifications to define meanings for Shape's operations. The first argument
of an abstract operation f modeling a corresponding concrete operation f is the class instance to
which f belongs. For example, referring to the above program fragment, recenter(c; p2) is the
abstract counterpart of c.recenter(p2).
We do not specify an abstract class, such as Shape, by means of a sort. Rather, we describe
relationships between the class' defined operations. The completeness of our specification is a
critical issue. Heuristically, we consider each pair, triple, etc. of member functions of Shape and
capture their mutual dependencies, if any, by algebraic equations. We remove obviously redundant
equations.
These specifications define the meanings of operations which manipulate objects of type Shape.
Using these specifications we may prove the correctness of the implementation of member functions
which are not pure virtual, by assuming the correctness of the "future" implementation of the
member which are pure virtual. As discussed earlier, the verification condition is
where the conjunct ensures that the argument of recenter remains constant.
The proof of the implementation of recenter relies on the pre- and post-conditions of Shape's
center and move operations. For such proofs to hold when recenter is passed an object whose
type is derived from Shape, the object's type must be a subtype, not merely a subclasses, of type
Shape. To show this, we must demonstrate that the relationships among the operations of Shape
hold for the operations and instances of Circle.
The specifications of Circle (shown below) differ from those of Shape, since the latter is a
classic abstract data type, rather than an abstract class in the C ++ sense. The first condition is the
class invariant. It ensures that every Circle has a non-negative radius.
Circle's operations can be annotated as usual [21], although the standard proof techniques for
imperative languages [11, 20] may fall short to prove object-oriented code.
We are concerned with a different problem here, that is, we want to prove that Circle is a
subtype of Shape. For this task we verify that the annotations of Shape hold for every instance
of Circle. This activity is similar to proving that Circle implements Shape with the technique
proposed in [19], with minor a difference-a Circle is a Shape, thus, no representation function
or equality interpretation is involved in the proofs.
Most of these proofs are easily formulated as problems for our theorem prover and completed
automatically.
Designing Specifications for Annotations
The problems discussed in the previous sections are formulated and resolved using first order
formulas. These formulas involve the symbols of a specification whose atomic components are
equations. In this section we discuss how we design both our equations and specifications. Our goal
is to produce equations and specifications that are easy to process automatically. The processing
is not limited to proving the formula expressing the correctness of a piece of software, but also
includes analyzing the specifications to determine that they satisfy properties whose absence is
often a sign of flaws.
A major obstacle to automation is the declarative nature of equations. Changing equations into
rewrite rules makes a specification more operational and simplifies the problem.
3.1 Rewriting
The unrestricted freedom, provided by equational reasoning, of replacing a term with an equal term
leads to a combinatorial explosion of possibilities which are hard to manage by a prover, whether
automated or human. An equation t can be "oriented" yielding a rewrite rule This
rewrite rule still defines the equality of t 1 and t 2 . It allows the replacement of an instance of t 1
with the corresponding instance of t 2 , but forbids replacement in the opposite direction. Orienting
equations transforms an algebraic specification into a term rewriting system [10, 26].
There are two crucial properties that must be achieved when equations are oriented. Two
terms provably equal by equational reasoning, should have a common reduct, i.e., a third term
to which both can be rewritten. This property is referred to as confluence or Church-Rosser. In
addition, it should not be possible to rewrite a term forever, in particular there should be no
circular rewrites. This property is referred to as termination or Noetherianity. A system with both
properties is canonical or complete or convergent. The Knuth-Bendix completion procedure [27]
attempts to transform an equational specification into a complete rewrite system. The termination
of the procedure cannot be guaranteed and its execution may require human intervention. The
difficulty stems from the undecidability of whether or not a rewrite system is canonical [9, 22].
For this reason, we do not attempt to convert an equational specification in the corresponding
complete rewrite system. Rather, we ask specifiers to structure their specifications as rewrite
systems with the above characteristics. The task is eased considerably by two strategies used in designing
a specification. The technique also ensures other properties, such as sufficient completeness,
which we deem essential in our framework.
3.2 Sufficient Completeness of Constructor-Based Systems
To apply our technique we consider only constructor-based systems, i.e., we partition the signature
symbols into constructors and defined operations. The constructors of a type T generate all the
data instances or values of T which are represented by terms, called normal forms, that cannot be
reduced. Terms containing defined operations represent computations. For example, the constructors
of the natural numbers are 0 and successor (denoted by the postfix "+1" in the examples).
The constructors of the type stack discussed in Example 2 are newstack and push, since any stack
is either empty or is obtainable by pushing some element on some other stack. Concat and reverse
are examples of defined operations.
Considering constructor-based systems raises the problem of sufficient completeness, yet another
undecidable property [25]. For the specification of type T to be sufficiently complete, it must assign
a value to each term of type T [18]. If the specification is structured as a constructor-based rewrite
system, sufficient completeness is equivalent to the property that normal forms are constructor
terms. If left sides of axioms have defined operations as their outermost operators and constructor
terms as arguments, we can state necessary and sufficient conditions for the sufficient completeness
of a specification.
A constructor enumeration [7] is a set, C, of tuples of constructor terms such that substituting
constructor terms for variables in the tuples of C exhaustively and unambiguously generates the set
of all the tuples of constructor terms. The set of tuples of arguments of a defined operation should
be a constructor enumeration. For example, the set of tuples of arguments of drop, discussed in
Example 2 and shown below
is a constructor enumeration of hnat; stacki, since every pair hx; yi, with x natural and y stack is
an instance of one and only one element of C.
The set of tuples of arguments of the operation max 0 discussed in Example 1 is not a constructor
enumeration, since h0; 0i is an instance of both h0; ii and hi; 0i. The second axiom of should
have been
Although the difference does not affect the specification, the latter axiomatization removes a (triv-
ial) ambiguity. Note that if the right side of the second axiom of were defined
than i, the specification would be inconsistent since would be a consequence of the axioms.
An operation is overspecified when two rules can be used to rewrite the same combination of
arguments. It is underspecified when no rule can be used to rewrite some combination of arguments.
Overspecification can be detected by a superposition algorithm [27] which uses unification to detect
overlapping. Underspecification is a natural condition for some operations, although it creates
non-negligible problems. It can be systematically avoided, for example, in the framework of order-sorted
specifications [15]. Underspecification can be detected by an algorithm informally described
below [23]. Operations that are not underspecified are called completely defined.
Huet and Hullot devised an algorithm to detect incompletely defined operations. This algorithm
assembles the arguments of the axioms into tuples and the terms in the i th position of each tuple
are checked to see that they include a variable or "an instance of each constructor." For each
constructor c, tuples of remaining arguments with constructor c or a variable in position i are
formed and recursively tested. A rigorous description appears in [23].
By way of example, we execute this algorithm with the set C as input. For constructor 0
in position 1, tuple 1 is considered. The set of tuples of remaining arguments, fhsig, is trivially
complete. For constructor successor in position 1, tuples 2 and 3 are considered. The set of tuples
of remaining arguments is fhnewstacki; hpush(s; e)ig. It contains an instance of each constructor of
stack in position 1. The completeness of each recursive problem, fhig from newstack and fhs; eig
from push, is obvious.
To ensure the confluence of a constructor-based specification it is sufficient to avoid overspecifi-
cation. To ensure sufficient completeness it is necessary, but not sufficient, to avoid underspecifica-
tion. If all operations are completely defined and terminating, then the specification is sufficiently
complete. In fact, every term has a normal form which obviously contains only constructor symbols
because any term containing a defined operation is reducible. Underspecification and overspecification
are easily checked syntactic properties. However, the termination of a rewrite system is
undecidable [9]. In the next section, we discuss syntactic properties sufficient to ensure termination
and show how to obtain them through our design strategies.
3.3 Design Strategies for Axioms
Confluence and sufficient completeness are undecidable, although essential, properties of a spec-
ification. Lack of confluence implies that some computation is ambiguously specified. Lack of
sufficient completeness implies that some computation is unspecified. We regard both conditions
as serious flaws of a specification. We describe two design strategies for generating confluent and
sufficiently complete specifications.
The binary choice strategy is an interactive, iterative, non-deterministic procedure that through
a sequence of binary decisions generates the left sides of the axioms of a defined operation. We
used the symbol " ", called place, as a placeholder for a decision. Let f be an operation of type
Consider the template th place has sort s i . To get a rule's
left side we must replace each place of a template with either a variable or with a constructor term
of the appropriate sort. In forming the left sides, we neither want to forget some combination of
arguments, nor include other combinations twice. That is, we want to avoid both underspecification
and overspecification. This is equivalent to forming a constructor enumeration.
We achieve our goal by selecting a place in a template and chosing one of two options: "variable"
or "inductive." The choice variable replaces the selected place with a fresh variable. The choice
inductive for a place of sort s i splits the corresponding template in several new templates, one for
each constructor c of sort s i . Each new template replaces the selected place with c(
there are as many places as the arity of c. A formal description of the strategy appears in [3].
We apply the strategy for designing the (left sides of the) rules of the operation drop discussed in
Example 2. The initial template is
We chose inductive for the first place. Since the sort of this place is natural, we split the template
into two new templates, one associated with 0 and the other with successor
We now chose variable for the remaining place of the first template and variable again for the first
place of the second template to obtain:
We chose inductive for last remaining place. Since the sort of this place is stack, we again split
the template in two new templates, one associated with newstack and the other with push. We
obtain:
For each remaining choice, variable is selected, completing the rules' left sides.
We now describe the second strategy, which ensures termination. The recursive reduction of a
term t is the term obtained by "stripping" t of its recursive constructors. A constructor of sort s
is called recursive if it has some argument of sort s. For example, successor and push are recursive
constructors. "Stripping" a term c(t is a derived operation and t i is a recursive
constructor, removes the outermost application of the constructor from t i . The stripping process is
recursively applied throughout the term. A formal description of the recursive reduction function
appears in [3]. We show its application in examples.
For reasons that will become clear shortly, we are interested in computing the recursive reduction
of the left side of a rewrite rule for use in the corresponding right side. The symbol "$" in the right
side of a rule denotes the recursive reduction of the rule's left side. With this convention, the last
axiom of drop is written
since the recursive reduction of the left side is drop(i; s). We obtain it by replacing i +1 with i since
i is the recursive argument of successor, and by replacing push(s; e) with s since s is the recursive
argument of push. When a constructor has several recursive arguments the recursive reduction
requires an explicit indication of the selected argument. We may also specify a partial, rather than
complete, "stripping" of the recursive constructors.
The recursive reduction strategy consists in defining the right sides of rules using only functional
composition of symbols of a terminating term rewriting system and the recursive reduction of the
corresponding left sides. If a specification is designed using the binary choice and the recursive
reduction strategies, then it is canonical and sufficiently complete [3].
3.4 Design Strategies for Specifications
The above strategies lead naturally to the design approach called stepwise specification by extensions
[12]. Given a specification S i , a step extends the specification by adding some operations
and yielding a new specification S i+1 . S i+1 is a complete and consistent extension of S i [12], if
every data element of S i+1 was already in S i and distinct elements of S i remain distinct in S i+1 .
Furthermore, if S i is canonical and sufficiently complete, then so is S i+1 [3].
We clarify these concepts by showing the steps yielding the specification of Example 2. Our
initial specification, S 0 , consists of the sorts boolean, natural and stack with their constructors
only, i.e., true, false, 0, successor, newstack, and push. Since there are no rewrite rules, i.e., the
constructors are free, the canonicity and sufficient completeness of S 0 are trivially established. Now
we extend S 0 with the operation concat obtaining S 1 .
concat(push(s;
The recursive reduction of the left side is concat(s; t). Since we designed the concat axioms using
the binary choice and recursive reduction strategies, S 1 is a complete and consistent extension of
S 0 and is a canonical and sufficiently complete specification. During this step we may also extend
take, size, and isnewstack. However, we cannot extend S 0 with reverse because
the right side of one axiom of reverse contains concat. We must first establish the properties of
the specification containing concat. Hence, a separate step is necessary. Then, we extend S 1 with
the operation reverse obtaining S 2 .
newstack
Our strategies together with the stepwise approach ensure again that S 2 is a complete and consistent
extension of S 1 and is a canonical and sufficiently complete specification. All the specifications
presented in this note are designed in this manner.
The binary choice strategy force us to construct left sides of plausible axioms for which we
do not want to define a right side. We complete the definition of these "axioms" by placing the
distinguished symbol "?" in the right side. Other specification languages follow an equivalent
approach to control incompleteness. For example, Larch would declare as "exempt" any term
appearing as left side of one of the axiom we single out with "?" Our strategies can be used also in
the presence of non-free constructors. Some properties of specifications with non-free constructors,
such as confluence, are no longer automatically guaranteed, but they can be checked more easily
than when no strategies at all are used in the design of the specification [3].
Proving Theorems About Annotations
The examples in the previous section contain many small theorems that need to be proved. Automating
these proofs makes them easier to carry out and less prone to error. In this section we
report our experience with this task.
4.1 Induction
Many equations, e.g., cannot be proved by rewriting, i.e., using only equational
reasoning. Such equations can be proved via structural induction [6] or data type induction [19].
Inductive variables of type T are replaced by terms determined by T 's constructors and inductive
hypotheses are established. If F is a formula to be proved, v is the inductive variable, and s is the
type of v, our induction proofs are carried out in the following manner. For every constructor c of
Skolem constant; and if s is an inductive hypothesis.
4.2 An Automated Theorem Prover
We have implemented a prototype theorem prover incorporating many concepts from the Boyer-Moore
Theorem Prover [5]. However, except for built-in knowledge of term equality and data type
induction, the knowledge in the theorem prover is supplied by specifications. Our theorem prover
checks that each function is completely defined by executing Huet's inductive definition. During
this check it identifies as "inductive" those arguments filled by instances of constructors. The
discovery of inductive arguments allows the prover to generate automatically the theorems which
constitute the cases of a proof by induction.
The theorem prover executes four basic actions: reduce, fertilize, generalize, and induct. Reduce
applies a rewrite rule to the formula being proved. Fertilize is responsible for "using" an inductive
hypothesis (i.e., replacing a subterm in the current formula with an equivalent term from an inductive
hypothesis). Generalize tries to replace some non-variable subterm common to both sides of
the formula with a fresh variable. Induct selects an inductive variable and generates new equations.
An induction variable is chosen from the set of the inductive arguments by heuristics which include
popularity [5] and seniority.
The theorem prover computes a boolean recursive function, called prove, whose input is an
equation and whose output is true if and only if the equation has been proved. Axioms and lemmas
of the specification are accessed as global data. Proofs of theorems are generated as side effects of
computations of prove. Users may override the automatic choices, made by the prover, for inductive
variables and generalizations. A technique discussed later allows users to use case analyses in proofs.
function prove(E) is
begin
if E has the form x = x; for some term x; then return true; end if;
if E can be reduced, then return prove(reduce(E)); end if;
if E can be fertilized, then return prove(fertilize(E)); end if;
contains an inductive variable, then
return
return false;
An attempt to prove a theorem may exhaust the available resources, since induction may generate
an infinite sequence of formulas to be proved. However, the termination property of the rewrite
system guarantees that an equation cannot be reduced forever and the elimination of previously
used inductive hypotheses [5] guarantees that an equation cannot be fertilized forever.
5 Experience Proving Theorems
All the proofs discussed in the previous sections have been completely generated with our theorem
prover, except for two proofs of inheritance properties. Many proofs were produced automatically
by the prover. Others were generated only after we supplied additional lemmas, independently
proved using the theorem prover.
The validation proofs for power functions for both while statement examples were all done
automatically, some with just term rewriting and the others with rewriting and induction. The
minimization proofs were slightly more challenging. Those for the array example required three
simple lemmas (e.g., to be proved and added to the set of axioms before the
theorem prover could finish the proofs. The lemmas were suggested by the similarity of terms on
opposite sides of the equations generated by the theorem prover. Generalization had to be inhibited
to obtain the minimization proofs for the stack example, as explained below. Relationships between
different Skolem constants inserted at the same time may be lost when generalization replaces terms
containing these constants with new constants. In attempting to verify
we generate the equation
Generalization replaces size(A1) with a new Skolem constant B2 and starts to verify the lemma
The relation between A1 and B2, lost by the generalization, is crucial to the validity of the theorem.
In nested inductions, for equation is rewritten to
and the proof attempt fails. Simply inhibiting generalization in this case solves the problem and
the theorem is proved with just rewriting and induction.
However, generalization is essential to other proofs. We illustrate this by an example, which
also shows how we discover the lemmas that make some proofs possible or simpler. The proof of
the total correctness of Example 2 requires verifying
During an induction on s, the formula to be proved becomes
The prover simultaneously generalizes reverse(take(size(A1); A1)) and push(newstack; A2) and
attempts to prove
The proof is easily completed by nested inductions on A6 and A7. Without generalization, the
proof continues by induction on A1, but the inductive hypothesis is not strong enough to complete
the proof. The prover keeps generating new inductions on formulas with increasing complexities
until the available resources are exhausted.
We regard generalized formulas as lemmas. Often we are able to further generalize the lemmas
suggested by the prover. For example, equation (4) suggests that newstack might be a right identity
of concat. Thus we prove
and use it as a lemma in the original proof. This immediately reduced the original formula to
The presence of a leading reverse on each side of the equation suggests that the equality may
depend on the arguments only. Thus we attempt to prove
The proof succeeds and we use this result as a lemma in the original proof. With these two
lemmas the original proof becomes trivial. Both lemmas are obtained by "removing context."
Generalization hypothesizes that the truth of an equation does not depend on certain internal
specific portions of each side. The latter example hypothesizes that the truth of an equation does
not depend on certain external specific portions each side, i.e.,
A proof of the conditions required for the semantic correctness of the generic instantiations of
accumulator was attempted for the operations max 0 (see Example 1), addition, multiplication, and
exponentiation. The theorems relative to the first three instantiations were all proved automatically.
However, the attempt to prove the associativity of exponentiation fails. The prover attempts to
verify by a nested induction. For the equation is reduced to
the prover halts with a message that it failed for this case. Thus, only the first three instantiations
of the generic accumulator are semantically correct. Interestingly, the fact that equation (3) holds
when step is associative and init is its left identity was proved automatically by our prover too.
The reversal of a stack discussed in Example 2 can be parallelized by a divide-and-conquer
technique similar to that discussed for accumulation. This program is an instance of a more
complex case of accumulation, in which the type of the result of the accumulation differs from the
type of the of elements of the accumulated sequence. We may exploit parallelism if we assume that
a stack is dynamically allocated in "chunks." Each chunk consists of a fixed-size array-like group of
contiguous memory locations, which are addressed by an index. Chunks are allocated on demand
and do not necessarily occupy contiguous locations of memory, rather are threaded together by
pointers as in a linked list. We reverse a stack in parallel only when the stack consists of several
chunks. In this case, we split the stack in two non-empty portions, say x and y, of linked together
whole chunks. We assume that the bottommost chunk of x points to the topmost chunk of y. We
reverse this link and recursively reverse x and y. When a portion of a stack consists of a single
chunk, we only have to swap the content of the chunk's memory locations to achieve reversal. The
correctness of this parallel implementation of a stack reversal relies on the equation
where reverse and concat were defined in Example 2. Operationally, concat stands for the operation
linking together two portions of a stack represented by its arguments. Reverse is overloaded: on
multi-chunk stacks it partitions and recurs whereas on single-chunk stacks it swaps. The proof of the
equation entails only the mutual relationships between these symbols, not their implementations.
Thus, the representation "in chunks" of the type stack is not an issue of the proof. Obviously, in a
comprehensive proof of correctness the differences between the two computations associated to the
reverse must be accounted for, e.g., as discussed in Section 2.2.
Our prover proves the above equation without human help. Interestingly, during the proof,
which is by induction on x, the prover automatically generates and proves an independent lemma
for each case of the induction. One lemma states that newstack is a right identity of concat, the
other that concat is associative.
In Section 2.4, we presented annotations involving the C ++ predefined type double. We did not
axiomatize this type by means of an algebraic inductive specification, and consequently we could
not use our prover for theorems relying on intrinsic properties of this type. However, all the proofs
in this section, except left(S) - right(S) and bottom(S) - top(S), were easily proved when we
provided some simple unproved lemmas, such the commutativity of "+" for double.
5.1 An Informal Comparison
The need to supply guidance to an automatic prover is not a peculiarity of our implementation.
For example, the Larch Theorem Prover (LP) [13] is designed to be a proof checker as well as an
automated prover. We consider this a approach very sensible.
The guidance required by our prover is in the form of lemmas. Lemmas simplify proofs and
improve understanding by "removing context." In our case they also overcome the lack of certain
proof tactics and of a friendly interface in our implementation.
We briefly compare how LP and our prover prove two sample theorems proposed in [13]. The
proofs involve the types linear container and priority queue, whose axioms are shown below, a total
order, and the type boolean with standard operators.
member
next
next(insert(Q;
else if next(Q) ! C then next(Q)
else C
The "?" symbol in the axioms of next corresponds to the Larch declaration "exempt" for next(new).
LP was used to prove the theorems:
E)
E)
The first theorem was proved after an inductive variable (C) was explicitly picked. The second
theorem required more intervention after rewriting produced:
LP was given a series of commands to divide the proof into cases and apply critical-pairs comple-
tions. The case isempty(Q) required a critical-pairs completion. The case :isempty(Q) required
case analysis on the truth V ! next(Q). Each case was further subdivided based on the truth
of . For the case :(V ! next(Q)) and critical-pairs completion was
requested.
Our prover also verified both these theorems, the first automatically and the second after we
added a few lemmas to the axioms. Since our prover's only knowledge derives from axioms, we do
not treat conditional expressions or implications in any special manner. They are represented by
means of user-defined operations. For example, implication is defined by the following axioms.
true
false
Thus we often need lemmas to manipulate these functions.
Since our prover handles only equations, we formulate the second theorem as
The prover automatically chooses A0 as the inductive variable. The base case, new, is
trivially proved by rewriting. The inductive case,
true as an inductive hypothesis and reduces the left side to
where - is a large nested conditional expression. We use two "standard" lemmas to simplify -. One
distributes "!" with respect to conditionals, i.e., we replace instances of x ! if b then y else z
with if b then x ! y else x ! z. This transformation allows the use of properties of the ordering
relation "!" such as irreflexivity and the "implied equation" [13, Fig. 9]. The other lemma splits
implications whose antecedent is a disjunction, i.e., we replace instances of x - y ) z with
z)- (y ) z). This transformation allows the use of each antecedent independently. By applications
of these lemmas, left side of the equation to be proved becomes
Now we enable the use of the antecedent of each conjunct of the formula by means of two "specific"
lemmas. This approach is directly inspired by [5]. One lemma replaces instances of
with the other lemma replaces instances Q
holds. The specific instance of the latter is member(A2; A1) =? i.e., the
contrapositive form of the first theorem proved for this problem.
After several inference steps, the left side is reduced to:
Now, we continue by cases on next(A2) ! A3 because this expression and its negation appear in
the formula. Although, our prover lacks a "proof-by-cases" tactic, we can simulate it by a lemma.
If P is the formula being proved and x is a boolean subexpression of P , we use a lemma to rewrite
P to In x ) P , we can replace the subexpression x of P by any y that is
known to be implied by x, and likewise for the other conjunct, that is reasoning by cases allows us
to cross-fertilize P [5]. Using this lemma triggers additional rewriting activity to transform the left
side to:
The conjunct with antecedent next(A2) ! A3 is rewritten as
fertilized with the inductive hypothesis, and reduced to true.
We continue by cases on member(A2; A1) because the truth of the theorem depends on standard
properties of ordering relations.
The first conjunct is rewritten to
where the consequent holds by the transitivity of "-". By successively reducing its consequents to
true, the second conjunct is eventually reduced to true.
true
Thus the proof terminates successfully.
The complexities of these proofs are comparable to those obtained with LP. All inductive variables
are chosen automatically, less case analysis is required, and there is no need to invoke the
Knuth-Bendix completion. Although this technique is occasionally useful, we find the proofs it
generates difficult to understand, and thus we prefer this tactic for situations that do not allow
data type induction, e.g., non constructor-based specifications.
We had to provide more lemmas to our prover. These lemmas are either trivial or instances
of trivial lemma schemas, although suggesting them requires "understanding the proof." This
is a mixed blessing. The effort to understand why a proof does or does not go through helps
discovering the relevant properties of a specification. This may lead to better specifications and
even code enhancements.
The user interface of our prover is very primitive. As a consequence we iterated our proof
attempt several times before completion and we had to create manually the instances of the lemma
schemas we supplied to the prover.
6 Concluding Remarks
We have discussed formal verification techniques for problems characterized by both differences
in sizes and addressed properties. Loops are the critical components of small programs. The
problems to be solved in this domain are correctness and termination, lack of expressiveness of
the axiomatizations used for annotations, and the inherent difficulty of reasoning about repeated
modifications of a program state.
Data type implementations are representative of medium size programs. The crucial problem to
be solved is the mutual internal consistency of a group of related subroutines bound by the choice
of the representation of abstract concepts by means of the structures offered by some hardware
architecture and/or some programming language. Proofs of correctness in this domain entail not
only the code, but also the representation mapping which has no physical presence in the software.
Module interconnection is the significant feature of large programs. Syntactic and semantic
commitments of one component may not match the expectations of another. This problem is exacerbated
by languages that allow the customization of a software unit by means of other units.
Proving correctness does not involve code directly, but annotations generated by proofs of correctness
for previous problems.
These tasks can all be addressed with a common formalism (equational specifications) and proof
techniques (rewriting and induction). In particular, their formalizations are based on specifications
that from a qualitative (and to some extent quantitative) point of view are independent of the tasks
and of their sizes. Furthermore, we have discussed conceptual and practical tools for designing and
using these specifications.
A crucial requirement of any specification is its adequacy. The assumption that a specification
is "good" is often mistaken unless considerable care is devoted to its design. Several properties,
unfortunately undecidable, are generally used to address the quality of a specification. We have
shown that, by restricting the expressive power of our specification language, the most common
and fundamental of these properties can be guaranteed. It is hard to say whether our restrictions
are too severe, but it is encouraging to discover that typical verification problems proposed in the
literature do not pose severe problems and that the proposed specifications are easy to use for both
humans and an automated tool.
Rewriting is the fundamental idea behind our approach. The design strategies we have presented
for designing rewrite rules ensure properties of the smaller units of specifications, the defined
operations. Our strategies also allow us to build specifications incrementally in a way that preserves
the properties of smaller units. In building large specifications from smaller ones, we glossed over the
problems of modularizations and parameterization of specifications. Our approach is compatible
with various techniques proposed for these features. In this respect, the properties we are able
guarantee ease the composition of specifications.
The hardest task of nearly any verification problem is proving theorems. Informal proofs are
easier to understand than formal ones, but are less reliable. Formal proofs, except for the simplest
problems, are too complicated for humans without automated tools. Our proofs contain a few
hundreds inferences, the majority of which are simple rewriting steps. Our prover becomes more
effective with occasional hints. The lemmas we supply are "macro-steps" that the prover, for lack
of knowledge and experience, would not carry to completion in certain contexts.
Finding the appropriate lemmas is not always easy. However, some lemmas such as those
discussed in our comparison with LP are relatively standard. Others are suggested by the prover
itself through generalization. From generalizations we sometimes find more elegant lemmas. Finally,
by inspecting proof attempts, we are able to detect repeated patterns or formulas of increasing
complexities which generally lead to proof failures. When these conditions arise, we look for lemmas
that overcome the problems.
We believe that our specification approach is adequate for a large number of cases. However,
our prover still fails to solve most non-trivial problems autonomously. It manages the bookkeeping
of inductions and it provides hints for necessary lemmas. It completely removes the tedium of
rewriting and the clerical mistakes associated with this activity. It prints readable proofs, although
sometimes it makes inferences that are not necessary because the prover's rewrite strategy is in-
nermost. An outermost rewriting strategy would produce shorter and more readable proofs. It
shows a remarkable skill in finding inductive variables. Despite the considerable limitations in its
user interface and proof tactics, the prover increases the quality of our specifications and enhances
considerably the human ability to produce formal proofs for software problems.



--R

A parallel object-oriented language with inheritance and subtyping
Automatically provable specifications.
Design strategies for rewrite rules.
On development of iterative programs from functional specifications.
A Computational Logic.
Proving properties of programs by structural induction.
Complexity analysis of term-rewriting systems
Mathematical Theory of Program Correctness.
Termination of rewriting.
Rewrite systems.
A Discipline of Programming.
Fundamentals of Algebraic Specifications 1: Equations and Initial Semantics.
Debugging Larch shared language specifications.
IEEE Computer
Operational semantics of order-sorted algebras
Introducing OBJ3.
Notes on type abstraction.
The algebraic specification of abstract data types.
Abstract data types and software validation.
An axiomatic basis for computer programming.
Proof of correctness of data representations.
Confluent reductions: Abstract properties and applications to term-rewriting sys- tems
Proofs by induction in equational theories with constructors.
The expressive theory of stacks.
On sufficient-completeness and related properties of term rewriting systems
rewriting systems.
Simple word problems in universal algebras
Modular specification and verification of object-oriented programs
Family values: A semantic notion of subtyping.
A new incompleteness result for Hoare's system.
An introduction to the construction and verification of Alphard programs.
Verification of programs by predicate transformation.
--TR
Reusing and interconnecting software components
The expressive theory of stacks
Termination of rewriting
Complexity analysis of term-rewriting systems
A parallel object-oriented language with inheritance and subtyping
Debugging Larch Shared Language Specifications
Rewrite systems
rewriting systems
A New Incompleteness Result for Hoare''s System
Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
Abstract data types and software validation
An axiomatic basis for computer programming
Mathematical Theory of Program Correctness
A Discipline of Programming
Fundamentals of Algebraic Specification I
Modular Specification and Verification of Object-Oriented Programs
Operational Semantics for Order-Sorted Algebra
Design Strategies for Rewrite Rules

--CTR
Olivier Ponsini , Carine Fdle , Emmanuel Kounalis, Rewriting of imperative programs into logical equations, Science of Computer Programming, v.56 n.3, p.363-401, May/June 2005
Antoy , Dick Hamlet, Automatically Checking an Implementation against Its Formal Specification, IEEE Transactions on Software Engineering, v.26 n.1, p.55-69, January 2000
term rewriting;software tools;abstract data types;algebraic axioms;generic program units;representation functions;program verification;convergence;sufficient completeness;structural induction;boyer-moore prover;rewriting systems;while statements;verification tasks;abstract base classes;mechanical assistance;theorem proving