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₁: comm]]e s, s)
  • [[p |- C₁;C₂: comm]]e s = [[p |- C₂: comm]]e
    ([[p |- C₁: comm]]e s)
  • [[p |- if E then C₁ else C₂ fi: comm]]e s =
    if([[p |- E: boolexp]]e s, [[p |- C₁: comm]]e s, [[p |- C₂: 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