A Language with Assignment
- Declaration-free Pascal subset.
- Program = sequence of commands
- C: Command -> Store_|_ ->
Store_|_
- A command produces a new store from its store argument.
- Command might not terminate ("loop")
-> C[[C]]s = _|_.
- Followup commands will not evaluate
-> C[[C]]:Store_|_
-> Store_|_ is strict.
- Command sequencing is store composition
-> C[[C1; C2]](s) =
C[[C2]](C[[C1]]s)
-> C[[C1; C2]] = C[[C1]]
o C[[C2]]
(See Schmidt, Figures 5.1 and 5.2)
Author: Wolfgang Schreiner
Last Modification: October 14, 1997