Information Technology Reference
In-Depth Information
'
1
v '
2
'
2
v '
3
'
1
v '
3
' v '
'
1
v '
2
'
3
v '
4
'
1
;
'
3
v '
2
;
'
4
'
1
v '
2
'
3
v '
4
'
1
+
'
3
v '
2
+
'
4
'
1
;(
'
2
;
'
3
)
v
(
'
1
;
'
2
);
'
3
(
'
1
;
'
2
);
'
3
v '
1
;(
'
2
;
'
3
)
'v
;
'
;
' v '
' v '
;
'
;
v '
(
'
1
+
'
2
);
'
3
v
(
'
1
;
'
3
)+(
'
2
;
'
3
)
(
'
1
;
'
3
)+(
'
2
;
'
3
)
v
(
'
1
+
'
2
);
'
3
'
1
v '
1
+
'
2
'
2
v '
1
+
'
2
'
+
' v '
'
1
v '
2
spawn
'
1
v
spawn
'
2
'
1
v '
2
rec
:'
1
v
rec
:'
2
rec
:' v '
[
7!
rec
:'
]
'
[
7!
rec
:'
]
v
rec
:'
%
1
%
2
b
1
b
2
%
1
%
2
b
2
b
1
%
1
!
b
1
v %
2
!
b
2
%
1
?
b
1
v %
2
?
b
2
b
b
0
0
b
%
0
b
b
chan
% v
b
0
chan
%
0
' v '
0
(Example 11).
Table 5.
Ordering on behaviours:
received). There is no explicit law for renaming bound behaviour variables as we
shall regard
rec
0
:'
0
when they are
rec
:'
as being equal to
-equivalent.
t
5
The Methodology
So far we have illustrated the variety of type and eect systems that can be
found in the literature. Now we turn to explaining the individual steps in the
overall methodology of designing and using type and eect systems:
{
devise a semantics for the programming language,
{
develop a program analysis in the form of a type and eect system (this is
what Sections 2, 3 and 4 have given numerous examples of),
{
prove the semantic correctness of the analysis,
{
develop an ecient inference algorithm,
{
prove that the inference algorithm is syntactically sound and complete, and
{
utilise the information for applications like program transformations or im-
proved code generation.
Search WWH ::
Custom Search