Go backward to Summary (Semantics III)
Go up to Top
Go forward to Summary (Semantics V)
Summary (Semantics IV)
- Command
-
[[ |- L:=E: comm]] =
update([[ |- L: intloc]],
[[ |- E: intexp]] , )
-
[[ |- C;C: comm]] = [[
|- C: comm]]
([[ |- C: comm]] )
-
[[ |- if E then C else C
fi: comm]] =
if([[ |- E: boolexp]] ,
[[ |- C: comm]] ,
[[ |- C: comm]] )
-
[[ |- while E do C od:
comm]] =
where =
if([[ |- E: boolexp]] ,
([[ |- C: comm]] ), )
-
[[ |- skip: comm]] =
-
[[ |- call X: comm]] =
where = [[ |-X: comm]]
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: abstraction2.tex,v 1.1 1996/04/10 07:30:13 schreine Exp schreine