Information Technology Reference
In-Depth Information
of the implementation has to dier radically from the usual conjunctive struc-
ture of the specication, and the validity of the step must be checked by a more
substantial proof. You do not expect to build an engine that is fast, eco-friendly,
and cheap from three simpler components, each of which enjoy only one of these
properties. A mismatch with implementation structure can throw into question
the value of prior specication. But it should not; indeed, the value of specica-
tion to the user is greatest just when it is fundamentally and structurally simpler
than its delivered implementation.
The simplest implementable operator to dene is the conditional, in which the
choice between components
P
and
Q
depends on the truth or falsity of a boolean
expression
b
, which is evaluated in the initial state. So
b
can be interpreted as a
predicate
, in which all variables are replaced by their initial values.
b
=
df
if
b
then
P
else
Q
b
^ P
_
(
:
)
^ Q
b
All the mathematical properties of the conditional follow directly from this def-
inition by purely propositional reasoning.
The most important feature of a programming language is that which per-
mits the same portion of program to be executed repeatedly as many times as
desired; and the most general way of specifying repetition is by recursion. Let
X
) be the body of the
procedure, written in the given programming language, and containing recursive
calls on
be the name of a parameterless procedure, and let
F
(
X
is monotonic in the inclusion ordering of the sets of
observations desribed by predicates, and since these sets can be regarded as a
complete lattice, we can use Tarski's xed point theorem to dene the meaning
of each call of
X
itself. Since
F
X
as the weakest possible solution of the implication
X ) F
(
X
).
This denition applies also to recursively dened specications. Incidentally, if
F
is expressed wholly in programming notations, it will be a continuous function,
and an equivalent denition can be given as the intersection of a descending
chain of iterates of
applied to
true
.
A non-terminating recursion can all too easily be specied as a procedure
whose body consists of nothing but a recursive call upon itself. Our choice of
the weakest xed point says that such a program has the meaning
true
,apred-
icate satised by all observations whatsoever. The programmer's error has been
punished in the most tting way: no matter what the specication was (unless
it was also trivally
true
), it will be impossible to prove that the product is
correct. This interpretation of divergence does not place any obligation on an
implementor of the programming language actually to exhibit the full range of
allowable observations. On the contrary, the implementor may assume that the
programmer never intended the divergence, and on this assumption may validly
perform many useful optimisations on the program before executing it. As a
result of such optimisations, the program may even terminate, for example,
F
(
while
x
0
do
x
:=
x −
1) ;
x
:=
abs
(
x
) can be optimised to nothing,
because the optimiser assumes that the intention of the while loop was to ter-
minate, which only happens when
x
starts positive. The anomalous terminating
Search WWH ::
Custom Search