Information Technology Reference
In-Depth Information
by the eect information. This idea occurred already in [39,40,48] in the form of
an extended side eect analysis with polymorphism and subeecting.
t
4
Causal Type Systems
So far the annotations and eects have had a rather simple structure in that
they have mainly been sets. It is possible to be more ambitious in identifying
the \causality" or temporal order among the various operations. As an example,
we now consider the task of extracting
behaviours
(reminiscent of terms in a
process algebra) from programs in Concurrent ML by means of a type and eect
system; here eects (the behaviours) have structure, they may influence the type
information (as in Example 9), and there are inference rules for subeecting and
shape conformant subtyping. These ideas rst occurred in [27,29] (not involving
polymorphism) and in [2,33,34] (involving polymorphism); our presentation is
mainly based on [33,34] because the inference system is somewhat simpler than
that of [1] (at the expense of making it harder to develop an inference algorithm);
we refer to [1, Chapter 1] for an overview of some of the subtle technical details.
An application to the validation of embedded systems is presented in [32] where
a control program is shown not to satisfy the safety requirements.
Example 10. Adding Constructs for Communication.
To facilitate the communication analysis we shall add constructs for creating
new channels, for generating new processes, and for communicating between
processes over typed channels:
e
::=
j
channel
j
spawn
e
0
j
send
e
1
on
e
2
j
receive
e
0
Here
channel
creates a new channel identier,
spawn
e
0
generates a new parallel
process that executes
e
0
,and
send
v
on
ch
sends the value
v
to another process
ready to receive a value by means of
receive
ch
. We shall assume that there is
a special constant
()
of type
unit
; this is the value to be returned by the
spawn
and
send
constructs.
t
Example 11. Communication Analysis.
Turning to the communication analysis the annotations of interest are:
'
::=
j j '
1
;
'
2
j '
1
+
'
2
j
rec
:' j
b
chan
% j
spawn
' j %
!
j %
?
b
b
%
::=
jfgj%
1
[%
2
j;
'
j
j
jj
j
b
1
!
b
2
j
b
%
b
::=
int
bool
unit
chan
::=
8
(
1
; ;
n
)
:
b
b
The behaviour
is used for atomic actions that do not involve communication;
in a sense it corresponds to the empty set in previous annotations although it
Search WWH ::
Custom Search