imperative language: denotate assignment
Assignment is only possible with some way to persist the name-value binding. We can do this via a store.
When we perform assignment, the new store is no longer the same as the previous store, so we denote it as such:
∑ -> ∑' ^-------- assignment occurs, e.g. x=1
As such we preservelaws:
- Any name in a given environment (inclusive of store, ∑) evaluates to the same value.
- Any expression in a given environment (inclusive of store, ∑) evaluates to the same value.