Information Technology Reference
In-Depth Information
behaviour of the optimised program for negative
is allowed by the semantics,
and is entirely attributed to the fault of the programmer. Our theory of pro-
gramming, whose objective is to avoid non-termination, can aord to treat all
instances of non-termination as equally bad; and the whole theory can often be
simplied just by regarding them as equal.
After denition of the relevant programming concepts, the next stage in the
top-down exploration of the theory of programming is the formalisation and
proof of the mathematical properties of programs. The simplest proprieties are
those that can be expressed as algebraic laws, either equations or inequations;
they are often pleasingly similar to algebraic properties proved of the familiar
operators of the arithmetic of numbers, which are taught at school. For example,
it is well known that disjunction (used to dene non-determinism in program-
ming) is like multiplication, in that it is associative and commutative, with
false
serving as its unit and
true
as its zero. Furthermore, conjunction distributes
through disjunction, and so do most simple programming combinators, includ-
ing sequential composition (Table 1). Laws are the basis for algebraic reasoning
and calculation, in which professional engineers often develop considerable skill.
x
P _ Q
=
Q _ P
P _
(
Q _ R
)=(
P_Q
)
_R
P_
false
=
P
P _
true
=
true
P ^
(
Q _ R
)=(
P^Q
)
_
(
P^R
)
P
;(
Q_R
)=(
P
;
Q
)
_
(
P
;
R
)
(
Q_R
);
P
=(
Q
;
P
)
_
(
R
;
P
)
Table 1. Basic algebra of non-determinism.
The same principles of programming language denition apply to process
algebras, which have the observational variable
trace
in their alphabet. One of
the risks of interactive programming is deadlock; and the worst deadlock is the
process that never engages in any recordable action, no matter what events the
environment may oer to engage in at the same time. As a result, its trace is
always empty
0
=
df
(
trace
=
hi
)
This denition is equally applicable to the process STOP in CSP.
A fundamental operation of a process algebra is external choice
, which
allows the environment to choose between its operands by appropriate selection
of the rst event to occur. It has an astonishingly simple denition
P
+
Q
P
+
Q
=
df
(
P ^ Q ^
0
)
_
(
0
^
(
P _ Q
))
Search WWH ::
Custom Search