Go backward to
Typing Rules
Go up to
Top
Go forward to
Interpretation
Linear Type Annotation
See
Schmidt, FIgure 2.2
.
Linear form of well-typed trees.
Type assignments as subscribts.
Type attributes as superscripts.
Example
fun
A=1,
fun
B=(@
loc
1
=0)
in
while
B
do
loc
1
:= (A+2)
od
( (
fun
A=((1)
^int_{}
)
^intexp_{}
)
^{A:
intexp
}
dec
_{}
,
(
fun
B =
( ((@(
loc
1
)
^intloc_{}
)
^intexp_{}
=
((0)
^int_{}
)
^intexp_{}
)
^boolexp_{}
)
^{B:
boolexp
}
dec
_{}
)
^
p
1
dec
_{}
in
(
while
(B)
^boolexp_p
do
((
loc
1
)
^intloc_p
:=
((
A
)
^intexp_p
+(2)
^int_p
)
^intexp_p
)
^comm_p
)
^comm_p
)^
comm
p
= {A:
intexp
, B:
boolexp
}
Author:
Wolfgang Schreiner
Last Modification: April 2, 1998