Go backward to
Typing Rules
Go up to
Top
Go forward to
Typing Rules
Typing Rules
One typing rule for each construction of each syntax rule.
Conditions under which constructions are well typed.
Linear Notation (full type annotation):
((
loc
1
)
intloc
:=((0)
int
)
intexp
(
while
((@(
loc
1
)
intloc
)
intexp
=((0)
int
)
intexp
)
boolexp
(
do
(
loc
2
)
intloc
:=
((@(
loc
1
)
intloc
)
intexp
+
((1)
int
)
intexp
)
intexp
)
comm
)
comm
)
comm
.
Abbreviation (root type annotation):
loc
1
:= 0;
while
@
loc
1
=0
do
loc
2
:=@
loc
1
+1
od
:
comm
Author:
Wolfgang Schreiner
Last Modification: March 26, 1998