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
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: core.tex,v 1.3 1996/02/05 10:34:52 schreine Exp schreine