Information Technology Reference
In-Depth Information
P
1
) D
1
P
2
) D
2
P
1
^ P
2
) D
1
^ D
2
An even more powerful principle is that which justies the reuse of a previously
written library component, which has been fully described by the specication
L
.
P
L
We want to implement a program
which uses
to help achieve a specication
S
. What is the most general description of a design for
P
that will achieve this
goal in the easiest way? The answer is just
S _L
, as described by the proof rule
P ) S _ L
P ^ L ) S
The Boolean term
); indeed,
the above law, together with the inference in the opposite direction, is used
in intuitionistic logic to dene implication as an approximate inverse (Galois
connection) of conjunction. An implication is always a predicate, but since it is
antimonotonic in its rst argument, it will rarely be a program
The identication of programs with more abstract descriptions of their be-
haviour oers a very simple and general explanation of a number of important
programming concepts. For example, a non-deterministic program can be con-
structed from two more deterministic programs
S _L
is often written as an implication (e.g.,
L S
by simply stating that
you do not care which one of them is selected for execution on each occasion.
The strongest assertion you can make about any resulting observation is that it
must have arisen either from
P
and
Q
P
Q
. So the concept of non-determinism
is simply and completely captured by the disjunction
or from
P _ Q
, describing the set
union of their observations. And the proof rule for correctness is just the famil-
iar rule for disjunction, dening it as the least upper bound of the implication
ordering
P
1
) DP
2
)D
P
1
_ P
2
)D
In words, if you want a non-deterministic program to be correct, you have to
prove correctness of both alternatives. This extra labour permits the most gen-
eral (demonic) interpretation of non-determinism, oering the greatest opportu-
nities for subsequent development and optimisation.
Existential quantication in the predicate calculus provides a means of con-
cealing the value of a variable, simultaneously removing the variable itself from
the alphabet of the predicate. In programming theory, quantication allows new
variables local to a particular fragment of program to be introduced and then
eliminated. In a process algebra, local declaration of event names ensures that
the internal interactions between components of an assembly are concealed, as
it were in a black box, before delivery to a customer. Observations of such in-
teractions are denoted by some free variable, say
x
occurring in the formula
P
x
; on each execution of
P
x
this variable must have some value, but we do not
know or care what it is. The value and even the existence of the variable can be
concealed by using it as the dummy variable of the quantication (
9x:P
x
).
Search WWH ::
Custom Search