Example 6.5.1.
We expect that after running the following program, \(\CVar y\) has the value 3 and not 2.
{
int x;
x = 3;
{
int x;
x = 2;
}
y = x;
}
Section 6.5 Scopes (C0b)
At the moment, there is no way to declare local variables in C0. The program has to start in a state that already contains all variables that the program uses. In this section, we extend C0 to scopes that allow for declaring local variables.
To this end, we modify the block syntax to contain variable declarations. The statement list of a block is preceded by a (possibly empty) list of variable declarations. Each declaration consists of a type and a variable. In this section, the type does not matter yet, but in the next section, we will add a small type system to C0 and make use of the types. The new block rules look like this:
\begin{equation*}
\begin{array}{rclll}
\mathit{Stmt} \ni s \amp \syndef \amp \cdots \amp \cdots \amp \text{like before} \\
\amp | \amp \ABlock{x_1,\dots,x_m}{k_1,\dots,k_m,p} \amp \CBlock{k_1\ x_1; \dots k_m\ x_m; p} \amp \text{block with variables} \\
\amp | \amp \cleave \amp - \amp \text{dispose local variables } \\
\end{array}
\end{equation*}
where the \(k_i\) are scalar types, i.e. either pointers or ints which we formally introduce in Definition 6.6.4. Additionally, we require that the variable names are pairwise different.
To model scoping in the semantics, we need to work a little. As discussed informally in Chapter 4, when entering a block, for each local variable a new container is created. When leaving the block, the containers are de-allocated and the added variables disappear again.
To realize this behavior, we change our definition of the state to contain a stack of variable assignments. When entering the block, a new variable assignment that contains all variables declared in that block will be put on the stack. When leaving the block, the corresponding variable assignment will we removed from the stack. To be able to detect the end of the block in the semantics, we add the statement \(\cleave\) to the abstract syntax. This syntactical construct is artificial and only used in the semantics. The programmer cannot use it in their programs. Additionally, when entering a block, we also need to provision new containers for the local variables. This is done by the new rule [Scope].
\begin{equation*}
\config{\CSeq{\CBlock{k_1\ x_1; \dots k_m\ x_m; p_1}}p_2}{\rho_1,\dots,\rho_k;\mu}\steprel
\config{\CConcat{p_1}{\CSeq{\cleave}{p_2}}}{\rho_1,\dots,\rho_k,\rho_{k+1};\mu'}\quad\text{[Scope]}
\end{equation*}
with
\begin{align*}
\rho_{k+1}\amp=\{x_1\mapsto a_1,\dots,x_m\mapsto a_m\}\\
\mu' \amp=\mu[a_1\mapsto \indetval,\dots,a_m\mapsto \indetval]\\
\emptyset \amp=\{a_1,\dots,a_m\}\cap\domain\mu
\end{align*}
The third condition states that the addresses \(a_i\) need to be fresh: They must not exist in the memory assignment.
The leave rule terminates to a state in which the top-most variable assignment is removed from the stack and all addresses added in that block are removed from the memory assignment. These are all addresses in the image of the variable assignment that is being removed.
\begin{equation*}
\config{\CSeq\cleave p}{\rho_1,\dots,\rho_k,\rho_{k+1};\mu}\steprel \config{p}{\rho_1,\dots,\rho_k;\mu'}\quad\text{[Leave]}
\end{equation*}
with
\begin{equation*}
\mu'\defeq\mu|_{\funimage{\rho_1\cup\cdots\cup\rho_k}}
\end{equation*}
Finally, we need to adapt the functions for L- and R-evaluation to cope with stacks of variable assignments. All but the case for the L-evaluation for variables can be just lifted to stacks of variable assignments. The new L-evaluation for variables using variable assignment stacks just searches for the first occurrence of the variable name in the stack from top to bottom:
\begin{equation*}
\denotL{x}\rho_1,\dots,\rho_k;\mu =
\left\{
\begin{array}{ll}
\rho_k\,x \amp \text{if } x\in\domain{\rho_k} \\
\denotL{x}\rho_1,\dots,\rho_{k-1};\mu \amp \text{otherwise}
\end{array}
\right.
\end{equation*}
Let us put everything together and work through an example.
Example 6.5.2.
We will consider the derivation of the program of the example above on the state
\begin{equation*}
\rho=\{\CVar y\mapsto\adra\}\quad\mu\defeq\{\adra\mapsto ?\}
\end{equation*}
\begin{equation*}
\small
\begin{array}{llll}
\amp \langle\CPrg{\{int x; x = 3; \{ int x; x = 2; \} y = x;\}} \amp| \{\CVar y\mapsto \adra\};\{\adra\mapsto ?\}\rangle \amp \\
\steprel \amp \langle\CPrg{x = 3; \{ int x; x = 2; \} y = x;$\ \cleave$} \amp| \{\CVar y\mapsto \adra\},\{\CVar x\mapsto \adrb\};\{\adra\mapsto ?, \adrb\mapsto ?\}\rangle \amp \text{[Scope]} \\
\steprel \amp \langle\CPrg{\{ int x; x = 2; \} y = x;$\ \cleave$ } \amp| \{\CVar y\mapsto \adra\},\{\CVar x\mapsto \adrb\}; \{\adra\mapsto ?,\adrb\mapsto 3\} \rangle \amp \text{[Assign]} \\
\steprel \amp \langle\CPrg{x = 2; $\cleave\ $ y = x;$\ \cleave$ } \amp| \{\CVar y\mapsto \adra\},\{\CVar x\mapsto \adrb\}, \{\CVar x\mapsto\adrc\}; \amp \text{[Scope]} \\
\amp \amp\phantom| \{\adra\mapsto ?,\adrb\mapsto 3, \adrc\mapsto ?\}\rangle \amp \\
\steprel \amp \langle\CPrg{$\cleave$ y = x;$\ \cleave$ } \amp| \{\CVar y\mapsto \adra\},\{\CVar x\mapsto \adrb\}, \{\CVar x\mapsto\adrc\}; \amp \text{[Assign]} \\
\amp \amp\phantom| \{\adra\mapsto ?,\adrb\mapsto 3, \adrc\mapsto 2\}\rangle \amp \\
\steprel \amp \langle\CPrg{y = x;$\ \cleave$} \amp| \{\CVar y\mapsto \adra\},\{\CVar x\mapsto \adrb\}; \{\adra\mapsto ?,\adrb\mapsto 3\}\rangle \amp \text{[Leave]} \\
\steprel \amp \langle\CPrg{$\cleave$ } \amp| \{\CVar y\mapsto \adra\},\{\CVar x\mapsto \adrb\}; \{\adra\mapsto 3,\adrb\mapsto 3\}\rangle \amp \text{[Assign]} \\
\steprel \amp \config{\CTerm}{\{\CVar y\mapsto\adra\}; \{\adra\mapsto 3\}} \amp \amp \text{[Leave]}
\end{array}
\end{equation*}
