Information Technology Reference
In-Depth Information
An important example of concealment is that which occurs when a program
component
P
is sequentially composed with the component
Q
, with the eect
that
Q
does not start until
P
has successfully terminated. The assembly (denoted
P
;
Q
) has the same initial observations as
P
, and the same nal observations as
Q
. Furthermore, we know that the initial values of the variables of
Q
are the
P
same as the nal values of the variables of
. But in normal sequential programs
we denitely do not want to observe these intermediate values on each occasion
that execution of the program passes a semicolon. Concealment by existential
quantication makes the denition of sequential composition the same as that
of composition in the relational calculus
(
!
x
(
P
;
Q
)=
df
9 x: P
x;x
)
^ Q
(
x;
)
Here we have written
and its superscripted variants to stand for the whole list
of global variables in the alphabet of
x
. In a procedural programming
language sequential composition is the commonest method of assembling small
components. The denition given above shows that the properties of the assem-
bly can be calculated from a knowledge of its components, just as they can for
conjunction.
Surprisingly, sequential composition is like conjunction also in admitting an
approximate inverse, { a generalisation of Dijkstra's weakest precondition [Dijk-
stra].
P
and
Q
L n S
is dened as the weakest specication [Hoare & He] of a program
P
such that
. There is also a postspec-
ication, similarly dened. Such inverses can be invaluable in calculating the
properties of a design, even though they are not available in the eventual target
programming language.
In the explanation of stepwise composition of designs, we used conjunction to
represent assembly of components. Conjunction of program components is not
an operator that is generally available in a programming language. The reason
is that it is too easy to conjoin inconsistent component descriptions, to produce
a description that is logically impossible to implement, for example,
P
;
L
is guaranteed to meet specication
S
(
x
:=
x
+1)
^
(
x
:=
x
+2)
;
which equals
false
So a practical programming language must concentrate on operators like sequen-
tial composition, which are carefully dened by conjunction and concealment to
ensure implementability. Negation must also be avoided, because it turns
true
,
which is implementable, to
false
, which is not. That is why prespecications,
which are antimonotonic in their rst argument, cannot be allowed in a program-
ming language. But there is a compensation. Any operator dened without direct
or indirect appeal to negation will be monotonic, and the programmer can use
for the newly dened operator the same rules for stepwise decomposition that we
have described for conjunction. The whole process of software engineering may
be described as the stepwise replacement of logical and mathematical operators
used in specications and designs by the implementable operators of an actual
programming language. Ideally, each step should be small and its correctness
should be obvious. But in many interesting and important cases, the structure
Search WWH ::
Custom Search