Information Technology Reference
In-Depth Information
upon the logical techniques. In annotated type systems, as well as in the type
and eect systems considered below, the annotations are normally sets of some
kind, but linking up with abstract interpretation it should be possible to allow
more general annotations that are elements of a complete lattice (that is possibly
of nite height as in the \monotone frameworks" of data flow analysis); however,
this possibility is hardly considered in the literature except in the case of binding
time analysis where the binding times (e.g. static and dynamic) are partially
ordered, c.f. [13,24].
3
Type and Eect Systems
The typing judgements of type systems take the following general form: a type
is associated with a program (or an expression or a statement) relative to a type
environment providing the type (or type scheme) for each free variable; this also
holds for the typing judgements used for the annotated type systems presented
above. Eect systems can be viewed as an outgrowth of annotated type system
where the typing judgements take the following more elaborate form: a type
and
an eect
is associated with a program relative to a type environment. Formally,
eects are nothing but the annotations already considered, but conceptually,
they describe intensional information about what takes place during evaluation
of the program unlike what was the case above.
Subeecting and Subtyping
The literature has seen a great variation in the uses to which eects have been
put: collecting the set of procedures or functions called [41], collecting the set of
storage cells written or read during execution [40], determining what exceptions
can be raised during evaluation, and collecting the regions in which evaluation
takes place [44] to mention just a few. We begin by considering an analysis for
collecting the set of storage cells written or read during execution.
Example 4. Adding Imperative Constructs.
To facilitate the side eect analysis we shall add imperative constructs (resem-
bling those of Standard ML) for creating reference variables and for accessing
and updating their values:
e
::=
j
new
x
:=
e
1
in
e
2
j
!
x j x
:=
e
0
The idea is that
new
x
:=
e
1
in
e
2
creates a new reference variable
x
for use in
e
2
and initialises it to the value of
e
1
;asaboveweuse
to identify the creation
point. The value of the reference variable
x
can be obtained by writing
!
x
and
it may be set to a new value by the assignment
x
:=
e
0
. The type of a reference
Search WWH ::
Custom Search