Go backward to Summary (Semantics III) Go up to Top Go forward to Summary (Semantics V)

Summary (Semantics IV)

• Command
  • [[P |- L:=E: comm]]e s =
        update([[P |- L: intloc]]e,
        [[P |- E: intexp]]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
  • [[P |- call X: comm]]e s = r(s)
        where r = [[P |-X: comm]]e