Theorem proving and
software engineering
Dr. Lindsay’s survey of computer support for theorem proving
is a timely report on a rapidly expanding research area. The
purpose of this brief introduction is to indicate the potential
role of such systems in software engineering.
It is widely accepted that there is a crisis in software develop
ment: projects are difficult to estimate, frequently overrun,
and result in systems which have many errors and are difficult
to use. In fact, the crisis is one of the design task being beyond
the ad hoc methods used. As the scale of integration of hardware
increases, the design task is again becoming the critical
bottleneck. In such a crisis there is a danger that quack
remedies are offered. Peter Naur has likened the situation to
that in George Bernard Shaw‘s ‘Widowers‘ houses‘, where
almost any change is one for the better. Are mathematical
methods a panacea or a quack remedy? Neither! There are, in
fact, many useful approaches which will make contributions
to various application and/or development environments.
Specialist (’fourth-generation’) languages, Prolog, functional
languages, prototyping and others all have a contribution to
make.
What are ‘formal methods’? Typically they use a mathematically
based notation in which to record specifications and,
based on these, they have a notion of an implementation
satisfying a specification which is susceptible to proof. Specifications
can be as precise as the final code which implements
them but can also be far shorter and more tractable. One
technique is to use pre- and post-conditions which state properties
of the results required without indicating how they are
to be achieved. Another, probably more important, technique
is to describe the intended function in terms of data objects
which match the problem rather than the implementation
language or machine. A short specification written in mathematical
notation can be checked for (some forms of) internal
consistency. More importantly, it can be used as a precise
reference point for the justification of design. If such design
is undertaken step by step, the ability to detect errors early can
result in an increase in productivity.
There are three major approaches into which most formal
methods can be divided. That which fits the normal development
route most closely is to fix a specification notation but
to record design by bringing in features of the implementation
language. Such design steps give rise to ‘proof obligations’
which are sentences in a logical language: their discharge
justifies the design. An alternative approach is to make the
initial description a very clear, but probably hopelessly inefficient,
algorithm. This is transformed in a series of steps to a
workable program. Each transformation step is an instance of
one 0f.a number of general rules. A few of these are universal;
most have applicability conditions which again result in
proof obligations. A third, newer, approach extracts algorithms
from constructive proofs of the existence of a result satisfying
a specification.
Putting aside the differences between approaches, it is clear
that each needs proofs. Other related formal methods also
need proofs of theorems (for example verifying, against a
denotational semantics, that transformations do preserve
equivalence; justifying inference rules).
The formal development of a system might give rise to many
proof obligations. Each such proof obligation is a putative
theorem which needs proof; it might be long, but its proof is
likely to be rather shallow. An ideal would be an oracle to
which each such expression was offered: an answer of ‘yes,
theorem’ or ’no, falsifiable’ would be the sought for response.
It can be proved that no algorithm to play the part of this
oracle can be produced for reasonably rich theories. At the
other extreme, the most modest requirement would be for a
system to which one provided the expression and a list of
steps which was claimed to constitute a complete proof. This
time, the program is not difficult to write, but the detail required
in preparing its input makes it almost unusable. The
most realistic target is probably a program which has useful
places for the human and the machine.
Completely checked machine proofs have been produced
only for very small programs. By contrast, formal specifications
are now being used in leading-edge industrial companies and
have been written for some of the largest programming
languages in use. The verification systems discussed by Lindsay
will lead on to others with wider applicability. Software
engineers of the future will use these tools (on critical applications)
in the same way that engineers in other disciplines use
mathematics thought too complex by the first ‘pragmatic’
practitioners.
