Information Technology Reference
In-Depth Information
!
x
x
A precondition for termination of a program can be written as the antecedent
of a conditional
ok
!
ok
(
x <
27
^
)
)
The owner of a vending machine may specify that the number of
choc
events
in the
trace
must never exceed the number of
coin
events. And the customer
certainly requires that when the balance of coins over chocs is positive, extraction
of a chocolate will not be refused. Explicit mention of refusals is a precise way of
specifying responsiveness or liveness of a process, without appeal to the concept
of fairness. But there is nothing wrong with fairness: it can be treated simply by
allowing traces to be innite. A fair trace is then one that contains an innite
number of occurrences of some relevant kind of event. It is not an objective of
a programming theory to place nitary or other restrictions on the language
in which specications are written. Indeed, our goal is to place whole power of
mathematics at the disposal of the engineer and scientist, who should exercise
it fully in the interests of utmost clarity of specication, and utmost reliability
in reasoning about correctness. We will therefore allow arbitrary mathematical
statements as predicates: as in the mu-calculus, we will even allow the denition
of weakest xed points of monotonic predicate transformers.
In an observational semantics of a programming language, the meaning of
an actual computer program is dened simply and directly as a mathematical
predicate that is true just for all those observations that could be made of any
execution of the program in any environment of use. For example, let
z
be the entire alphabet of global variables of a simple program. The assignment
statement
x; y;
and
x
x
+1 has its meaning completely described by a predicate stating
that when it is started, the value of
:=
x
is incremented, and that termination occurs
x
provided the value of
is not too large. The values of all the other global program
variables remain unchanged
ok )
!
ok ^
!
y
=
!
x
=
!
z
=
y
^
x
< max ^
x
z
+1
^
Similarly, the behaviour of the deadlock process in a process algebra can be
described purely in terms of its trace behaviour { it never engages in any event,
and so the trace remains forever empty
trace
=
<>
(Here and in future, we will simplify our treatment of processes by ignoring issues
of divergence). This kind of denition of programming concepts enables us to
regard both specications and programs as predicates placing constraints on the
range of values for the same alphabet of observational variables; the specication
restricts the range of observations to those that are permitted; and the program
denes exhaustively the full range of observations to which it could potentially
give rise. As a result, we have the simplest possible explanation of the important
concept of program correctness. A program
P
meets a specication
S
just if
Search WWH ::
Custom Search