Information Technology Reference
In-Depth Information
The typing judgements have the form
Γ `
COM
e
:
&
'
where the type environ-
b
ment
Γ
maps variables to type schemes (or types),
isthetypescheme(ortype)
b
for the expression
e
,and
'
is the behaviour that may arise during evaluation of
e
. The analysis is specied by the axioms and rules of Tables 4 and have many
points in common with those we have seen before; we explain the dierences
below.
The axioms for constants and variables dier from the similar axioms in Table
3inthat
. A similar remark holds for the rule for function
abstraction. In the rule for function application we now use sequencing to express
that we rst evaluate the function part, then the argument and nally the body
of the function; note that the left-to-right evaluation order is explicit in the
behaviour.
is used instead of
;
The axiom for channel creation makes sure to record the program point in the
type as well as the behaviour, the rule for spawning a process encapsulates the
behaviour of the spawned process in the behaviour of the construct itself and the
rules for sending and receiving values over channels indicate the order in which
the arguments are evaluated and then produce the behaviour for the action
taken. The rules for generalisation and instantiation are much as before.
The rule for
subeecting
and
subtyping
is an amalgamation of the rules in Table
3 and Example 6. Also note that there is no
in the axiom for
channel
unlike
in the axiom for
new
in Table 3; this is because the presence of subtyping makes
it redundant. The ordering
%
0
on types is given by
b
b
1
b
2
' v '
0
0
0
b
%
0
1
2
b
b
b
b
b
b
b
b
'
!
b
'
0
!
b
chan
%
b
0
chan
%
0
1
2
b
1
2
b
b
'
!
b
and is similar to the denition in Example 6:
1
2
is contravariant in
1
b
b
but covariant in
'
and
2
,and
chan
%
is both covariant in
(for when a value
b
b
b
is sent) and contravariant in
(for when a value is received) and it is covariant
b
% %
0
means that
%
0
(modulo
in
%
. As before, the ordering
%
is \a subset of" of
' v '
0
on behaviours is more complex than what
has been the case before because of the rich structure possessed by behaviours.
The denition is given in Table 5 and will be explained below. Since the syntactic
categories of types and behaviours are mutually recursive also the denitions of
b
b
UCAI
). However, the ordering
' v '
0
need to be interpreted recursively.
The axiomatisation of
0
and
' v '
0
ensures that we obtain a preorder that is a con-
gruence with respect to the operations for combining behaviours. Furthermore,
sequencing is an associative operation with
as identity and we have a distribu-
tive law with respect to choice. It follows that choice is associative and commu-
tative. Next the axioms for recursion allow us to unfold the
-construct. The
nal three rules clarify how behaviours depend upon types and regions:
rec
b
chan
%
is both contravariant and covariant in
and is covariant in
%
(just as was the
b
case for the type
chan
%
);
%
!
is covariant in both
%
and
(because a value
b
b
b
is sent) whereas
%
?
is covariant in
%
and contravariant in
(because a value is
b
b
Search WWH ::
Custom Search