Go backward to The Semantics of Abstractions
Go up to Top
Go forward to The Semantics of Abstractions
The Semantics of Abstractions
- Command: [[C: comm]] in Environment ->
Store ->
Store_bottom
- [[p |- L:=E: comm]]e s =
update([[p |- L: intloc]]e,
[[p |- C_1: comm]]e s, s)
- [[p |- C_1;C_2: comm]]e s = [[p
|- C_2: comm]]e
([[p |- C_1: comm]]e s)
- [[p |- if E then C_1 else C_2
fi: comm]]e s =
if([[p |- E: boolexp]]e s,
[[p |- C_1: comm]]e s,
[[p |- C_2: comm]]e s)
- [[p |- while E do C od:
comm]]e s = w(s)
where w(s) =
if([[p |- E: boolexp]]e s,
w([[p |- C: comm]]e s), s)
- [[p |- skip: comm]]e s = s
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: abstraction.tex,v 1.1 1996/03/05 08:55:21 schreine Exp schreine