Environment and the Store

Before we can present a semantics for Cool we need a number of concepts and a considerable amount of notation. An environment is a mapping of variable identifiers to locations. Intuitively, an environment tells us for a given identifier the address of the memory location where that identifier's value is stored. For a given expression, the environment must assign a location to all identifiers to which the expression may refer. For the expression, e.g., $a + b$, we need an environment that maps $a$ to some location and $b$ to some location. We'll use the following syntax to describe environments, which is very similar to the syntax of type assumptions used in Section 12.

$$E = [ a:l_1, b:l_2]$$

This environment maps $a$ to location $l_1$, and $b$ to location $l_2$.

The second component of the context for the evaluation of an expression is the store (memory). The store maps locations to values, where values in Cool are just objects. Intuitively, a store tells us what value is stored in a given memory location. For the moment, assume all values are integers. A store is similar to an environment:

$$S = [ l_1\rightarrow 55, l_2\rightarrow 77 ]$$

This store maps location $l_1$ to value $55$ and location $l_2$ to value $77$.

Given an environment and a store, the value of an identifier can be found by first looking up the location that the identifier maps to in the environment and then looking up the location in the store.

$$\begin{array}{rcl} E(a) &=& l_1 \\ S(l_1) & = & 55 \end{array}$$

Together, the environment and the store define the execution state at a particular step of the evaluation of a Cool expression. The double indirection from identifiers to locations to values allows us to model variables. Consider what happens if the value $99$ is assigned variable $a$ in the environment and store defined above. Assigning to a variable means changing the value to which it refers but not its location. To perform the assignment, we look up the location for $a$ in the environment $E$ and then change the mapping for the obtained location to the new value, giving a new store $S'$.

$$\begin{array}{rcl} E(a) & = & l_1 \\ S' & = & S[99/l_1] \end{array}$$

The syntax $S[v/l]$ denotes a new store that is identical to the store $S$, except that $S'$ maps location $l$ to value $v$. For all locations $l'$ where $l'\not=l$, we still have $S'(l')=S(l')$.

The store models the contents of memory of the computer during program execution. Assigning to a variable modifies the store.

There are also situations in which the environment is modified. Consider the following Cool fragment:

  let c : Int <- 33 in
    c

When evaluating this expression, we must introduce the new identifier $c$ into the environment before evaluating the body of the let. If the current environment and state are $E$ and $S$, then we create a new environment $E'$ and a new store $S'$ defined by:

$$\begin{array}{rcl} l_c & = & newloc(S)\\ E' & = & E[l_c/c]\\ S' & = & S[33/l_c] \end{array}$$

The first step is to allocate a location for the variable $c$. The location should be fresh, meaning that the current store does not have a mapping for it. The function $newloc()$ applied to a store gives us an unused location in that store. We then create a new environment $E'$, which maps $c$ to $l_c$ but also contains all of the mappings of $E$ for identifiers other than $c$. Note that if $c$ already has a mapping in $E$, the new environment $E'$ hides this old mapping. We must also update the store to map the new location to a value. In this case $l_c$ maps to the value $33$, which is the initial value for $c$ as defined by the let-expression.

The example in this subsection oversimplifies Cool environments and stores a bit, because simple integers are not Cool values. Even integers are full-fledged objects in Cool.