next up previous contents
Next: An imperative programming language Up: Locations Previous: Basic defintion of locations


Updating the environment requires updating of a dependent function. We take advantage of the structure of environments, in particular that the number of storage cells can be compressed without losing information in order to construct an update function for which update_lemma is provable.

Current doesn't compile

Fri May 24 19:01:27 BST 1996