Information Technology Reference
In-Depth Information
cell for values of type
is
ref
and the underlying type system of Example 1
is extended with the rules:
Γ `
UL
!
x
:
if
Γ
(
x
)=
ref
Γ `
UL
x
:=
e
Γ `
UL
e
:
if
Γ
(
x
)=
ref
:
Γ `
UL
e
1
:
1
Γ
[
x 7!
1
ref
]
`
UL
e
2
:
2
Γ `
UL
new
x
:=
e
1
in
e
2
:
2
Example 5. Side Eect Analysis.
In the side eect analysis a reference variable is represented by a set
of program
points where it could have been created; this set is called a region and has the
general form
%
f
1
g[[f
n
g
which we write as the set
f
1
; ;
n
g
.The
annotations of interest are:
'
::=
f
!
gjf
:=
gjf
new
gj'
1
['
2
j;
%
::=
fgj%
1
[%
2
j;
'
!
b
::=
int
j
bool
j j
b
1
2
j
b
ref
%
b
Here
ref
%
is the type of a location created at one of the program points in
b
the region
%
; the location is used for holding values of the annotated type
.The
b
annotation
!
means that the value of a location created at
is accessed,
:=
means that a location created at
is assigned, and
new
that a new location
has been created at
.
The typing judgements have the form
Γ `
SE
e
:
&
'
. This means that under the
b
type environment
Γ
, if the expression
e
terminates then the resulting value will
have the annotated type
describes the side eects that might have taken
place during evaluation. As before the type environment
and
'
b
Γ
will map variables
to annotated types; no eects are involved because the semantics is
eager
rather
than
lazy
.
The analysis is specied by the axioms and rules of Table 3; these rules embody
the essence of eect systems. In the clauses for constants and variables we record
that there are no side eects so we use
for the overall eect. The premise of
the clause for function abstraction gives the eect of the function body and this
eect is used to annotate the arrow of the function type whereas we use
;
as
the overall eect of the function denition itself: no side eects can be observed
by simply dening the function. In the rule for function application we see how
the information comes together: the overall eect is what can be observed from
evaluating the argument
;
e
1
, what can be observed from evaluating the argument
e
2
, and what is obtained from evaluating the body of the function called.
Turning to the rules involving reference variables we make sure that we only
assign a value of the appropriate type to the reference variable. Also, in each of
Search WWH ::
Custom Search