Information Technology Reference
In-Depth Information
The language has expressions (or programs)
e
and types
given by:
e
::=
c j x j
fn
x
=>
e
0
j e
1
e
2
j
::=
int
j
bool
jj
1
!
2
Here
c
denotes a family of constants (each of type
c
),
x
denotes a family of
variables, and
is an identication of the function abstraction to be used in the
control flow analysis to be presented in Example 2.
The typing judgements of the underlying or original type system have the form
Γ `
UL
e
:
where the type environment
Γ
maps variables to types; the denition
is as follows:
Γ
[
x 7!
x
]
`
UL
e
0
:
0
Γ `
UL
c
c
:
Γ `
UL
fn
x
=>
e
0
:
x
!
0
Γ `
UL
e
1
:
2
!
0
Γ `
UL
e
2
:
2
Γ `
UL
x
:
Γ
(
x
)
Γ `
UL
e
1
e
2
:
0
That a function has type
1
!
2
means that given an argument of type
1
it
will return a value of type
2
in case it terminates.
t
Perhaps the simplest technique for extending the expressiveness of types is to add
annotations to the type constructors or base types. One popular class of analyses
that can be expressed using this technique consists of interprocedural control
flow analyses which track the origins of where functions might have been dened
[7,8,11]; this can be extended with components for tracking where functions
are applied and thus has strong similarities to the classical
use-denition
and
denition-use
analyses of data flow analysis.
Example 2. Control Flow Analysis.
To obtain a control flow analysis we shall annotate the function type
1
!
2
with information,
'
, about which function it might be:
'
::=
fgj'
1
['
2
j;
'
!
b
j
jj
b
1
2
b
::=
int
bool
So
will be a
set
of function names { describing the set of function denitions
that can result in a function of a given type.
The typing judgements of the control flow analysis have the form
'
Γ `
CFA
e
:
b
Γ
where the type environment
maps variables to annotated types. The judge-
ments are dened in Table 1; note that the clause for function abstraction an-
notates the arrow of the resulting function type with the information that the
abstraction named
of functions that could
be returned. In the presence of conditionals it is essential that we use
should be included in the set
fg['
fg['
Search WWH ::
Custom Search