In preceding articles, we considered functional programs that do not contain assignment or other operations that change the values of identifiers. In computer science, of course, it is more common to use imperative programs. A typical example of imperative construct is the assignment statement $x:=y$, which sets the value of $x$ to the value $y$.
In this article, we will introduce the simple imperative language of so-called $\text{while}$ programs, and give its operational semantics in a proof system manner.
While Programs
L-values and R-values
One basic property of C-like languages is that assignable variables have two kinds of “values.” These have traditionally been called L-values and R-values. They correpsond to occurrences on the left and right hand side of an assignment statememt.
In elementary terms, the L-value of a variable is its location in memory and the R-value is the contents of this location.
To see the reason to raise this concept, let us consider the assignment statement $x:=y+3$. A compiler for a register-based machine might compile this statement into the following instructions:
- Put the contents of location $y$ in register $a$.
- Add $3$ to register $a$.
- Store the contents of register $a$ in location $x$.
It is easy to see from this “compiled code” that the occurrence of $y$ on the right hand of the assignment refers to the contents of a location, while the occurrence of $x$ on the left refers to the location itself.
Another way of saying this is that the assignment $x:=y’+3$ will have the same effect as $x:=y+3$ if the contents of $y’$ is the same as $y$, but $x’:=y+3$ will have the same effect as $x:=y+3$ only if $x’$ names the same location of $x$.
In general, the type of the L-value of a variable is different from the type of its R-value — the L-value is a location, while the R-value may be an integer or other storable value.
In giving denotational semantics to programs, it is necessary to distinguish between L-values and R-values. This is not overly difficult, but it leads to slight technical complication since the distinction relies on context.
As a simplifying assumption, we will use a version of $\text{while}$ programs in which the distinction between L-values and R-values is explicit. Specifically, we will use variables of type $loc$ for assignable variables, and apply a contents function $cont$ to a location to extracts its contents.
This is similar to the way pointer variables are used in C, for example, where we write $\ast x$ for the contents of $x$.
This is also the way all variables are treated in the programming language ML, which does not seem to suffer from this approach. In fact, explicit location expressions in ML provides some useful flexibility.
Syntax of While Programs
For simplicity, we assume we are only interested in values of two basic types, $val$ and $bool$, and only elements of type $val$ may be stored.
In writing examples, it is helpful to regard $val$ as $nat$, and assume common numeric and boolean operations. However, when we analyze the logic for reasoning about $\text{while}$ programs, it will be useful to consider different semantic interpretations of $val$, and arbitrary algebraic functions over $val$ and $bool$.
Let $\Sigma$ be an algebraic signature over basic type $val$ and $bool$, and let us assume the function symbol
\[cont:loc \to val\]is distinct from the function symbols of $\Sigma$. It is a function that maps L-values to R-values.
To simplify syntactic considerations, let us choose some infinite sets $\Gamma_{loc}$, $\Gamma_{val}$ and $\Gamma_{bool}$ of types $loc$, $val$ and $bool$, respectively, and use these throughout our discussion of $\text{while}$ program.
Using algebraic terms of types $val$ and $bool$ over $\Sigma$ and function symbol $const$, we define the language of $\text{while}$ programs by
\[P \quad ::= \quad x:= M \mid P;\:P \mid \text{if } B \text{ then } P \text{ else } P \mid \text{while } B \text{ do } P \text{ od}\]where we assume that variable $x$ has type $loc$, expression $M$ has type $val$ and $B$ has type $bool$. And we allow arbitrary operations on $val$ and $bool$, such as $+$, $-$, $<$, and so on.
As an example, using this signature, we may write the logarithm program as the following.
\[x:=1 ;\: y:=0 ;\: \text{while } \: cont \: x < z \: \text{ do } \: x := cont \: x + cont \: x ; \: y := cont \: y + 1 \:\text{ od}\]We may think of this program as having input $z$ and output $y$. Note that we let $z$ has type $val$ instead of $loc$ because its value will not change during the whole program. This program uses a “scratch” variable $x$ to set $y$ to an integer approximation of the logarithm of any $z>0$. For easier understanding, we also put an equivalent C program here.
1
2
3
4
5
6
7
int logarithm(int z) {
while (x < z) {
x = x + x;
y = y + 1;
}
return y;
}
Operational Semantics
Basic Symbols and Expressions
Expressions in $\text{while}$ programs may contain variables from $\Gamma_{loc}$, $\Gamma_{val}$ and $\Gamma_{bool}$, the special function symbol $cont$, and function symbols from any two-sorted algebraic signature $\Sigma$.
To allow easy comparison between operational and denotational semantics, we assume we are given a two-sorted algebra $\mathcal{A}_0 = \langle \mathcal{A}^{val} ,\mathcal{A}^{bool},f^\mathcal{A},… \rangle$ for signature $\Sigma$, where $\mathcal{A}^{bool}$ is the two-element set ${ true,false }$ of booleans.
Since $\text{while}$ programs contain variables, we need an environment $\eta$ mapping variables from $\Gamma_{loc}\cup \Gamma_{val} \cup \Gamma_{bool}$ to elements of $\mathcal{A}$ of the appropriate type.
If location variables $x$ and $y$ are given the same location by the environment, then an assignment to $x$ will also change the contents of $y$. This effect, called aliasing, is important in reasoning about imperative programs.
Locations and Stores
Both the operational and denotational semantics of $\text{while}$ programs will involve data structures called stores. Intuitively, stores represent the “memory contents” of some simple machine. It depicts the current memory state of a machine — you can think of it as a mathematical function mapping each memory location in this machine to a specific value stored in there.
The concept stores can give a more detailed semantics for the function symbol $cont$, as we will see in the following.
We begin with an algebraic specification of the operations on stores, which will be useful for reasoning about programs.
We extend $\mathcal{A}_0$ to a four-sorted algebra $\mathcal{A}$ with locations and stores by letting $\mathcal{A}^{loc}$ be any countably infinite set, and letting $\mathcal{A}^{store}$ be the set of all functions from $\mathcal{A}^{loc}$ to $\mathcal{A}^{val}$. (A sort could also be a set of functions.) And we add function symbols $init$, $update$ and $lookup$ with the following types.
\[\begin{split} &init : store \\ &update: store \times loc \times val \to store \\ &lookup: store \times loc \to val \end{split}\]Note that we have restricted $\text{while}$ programs so that only elements of type $val$ may be stored.
Intuitively, $init$ is some distinguished store which might, for example, contain 0 in every location; $update$ is a function that changes the value associated with some location and return the changed stores; and $lookup$ reads the value stored in some location.
More precisely, we have the following interpretation for these operations with four variables $\mathscr{l}:loc$, \(\:\mathscr{l}':loc\), \(\:\mathscr{s}:store\), \(\:\mathscr{v}:val\):
- $init^\mathcal{A}$ is any constant function. So, arbitrary initialzation is allowed.
- $lookup^\mathcal{A}(\mathscr{s},\mathscr{l}) = \mathscr{s}(\mathscr{l})$.
- $update^\mathcal{A}(\mathscr{s},\mathscr{l},\mathscr{v})$ is the function $\mathscr{s}’$ that is identical to $\mathscr{s}$ except that $\mathscr{s}’(\mathscr{l}) = \mathscr{v}$. In other words, only the contents in location $\mathscr{l}:loc$ is changed.
The behavior of these functions is characterized by the following algebraic axioms:
\[lookup \: (update \: \mathscr{s} \: \mathscr{l}' \: \mathscr{v}) = \text{ if } \: Eq? \: \mathscr{l} \: \mathscr{l}' \: \text{ then } \mathscr{v} \text{ else } \: (lookup \: \mathscr{s} \: \mathscr{l})\tag*{($lookup$)}\] \[update \: \mathscr{s} \: \mathscr{l} \: (lookup \: \mathscr{s} \: \mathscr{l}) = s\tag*{$(update)_1$}\] \[\tag*{$(update)_2$} \begin{split} update \: (update \: \mathscr{s} \: \mathscr{l}\: \mathscr{u}) \: \mathscr{l}'\: \mathscr{v}= &\text{ if } \: Eq? \: \mathscr{l} \: \mathscr{l}' \: \text{ then } \: update \: \mathscr{s} \: \mathscr{l} \: \mathscr{v}\\ &\text{ else } update \: (lookup \: \mathscr{s} \: \mathscr{l}'\: \mathscr{v}) \: \mathscr{l}\: \mathscr{u} \end{split}\]It is easy to figure out their meanings after careful reading.
A common question is why we have seperated environment and stores, instead of using a single function mapping identifiers to values.
For programs that do not contain declarations, it is technially possible to give both operational and denotational semantics using only a single mapping. In some cases, this is the best approach, since there is less mechinery involved.
However, there are both intuitive and technical reasons for seperating environments from stores, as we do here.
An intuitive reason is that environments and stores are conceptually different, and correspond to different mechanisms in actual language implementation. The environment corresponds, roughly, to the symbol table that is used during the compilation to keep an association between program identifiers and memory locations. For $\text{while}$ programs, the entire program is understood with respect to a signle environment while the store changes during the program execution.
From a technical standpoint, we give denotational semantics by translating $\text{while}$ programs into lambda terms that manipulate the store explicitly. This translation is simplified by using the same form of environment for $\text{while}$ programs as lambda terms with store operations. This would not be possible if we did not seperate environments from stores in the semantics of $\text{while}$ programs.
Evaluation of Expressions
The operational semantics for $\text{while}$ programs has two parts. The first is a four-place realtion \(\stackrel{\text{eval}}{_\rightsquigarrow}\) between algebraic expressions, environments, stores and semantic values of algebraic terms. We will write this as an infix relation \(\langle M,\: s \rangle_\eta \stackrel{\text{eval}}{_\rightsquigarrow} v\) to suggest that we “evaluate” expression $M$ in store $s$ with respect to environment $\eta$ and obtain value $v$. To simplify the notation, we will omit the subscript for the environment and assume that we have chosen one fixed environment.
The approach we use is suited to programming languages with nondeterministic or non-terminating expressions. However, the expressions we use in $\text{while}$ programs are single-valued and terminating. Consequently, our evaluation relation is a total function.
To illustrate a general method for defining evaluation relations, we will present $\stackrel{\text{eval}}{_\rightsquigarrow}$ using a form of proof system.
There are two axioms for $\stackrel{\text{eval}}{_\rightsquigarrow}$, one for variables and one for constants. In words, the value of a variable is given by the environment, and the value of a constant is given by the algebraic structure $\mathcal{A}$.
\[\begin{split} \langle x,\: s \rangle &\stackrel{\text{eval}}{_\rightsquigarrow} \eta(x)\\ \langle c,\: s \rangle &\stackrel{\text{eval}}{_\rightsquigarrow} c^\mathcal{A} \end{split}\]There are two inference rules for compound terms, one for application of an algebraic function (interpreted by $\mathcal{A}$), and one for the special function $cont$ which accesses the store. The rule for algebraic functions is essentially a formalization of the way we define the meaning of an algebraic term.
\[\frac{\langle M_1,\: s \rangle \stackrel{\text{eval}}{_\rightsquigarrow} v_1,...,\langle M_k,\: s \rangle \stackrel{\text{eval}}{_\rightsquigarrow} v_k}{\langle fM_1...M_k,\: s \rangle \stackrel{\text{eval}}{_\rightsquigarrow} v} \text{ , where } f^\mathcal{A}(v_1,...,v_k)=v.\]The value of $cont$ $x$ is determined by looking up location $x$ in store.
\[\frac{\langle x,\: s \rangle \stackrel{\text{eval}}{_\rightsquigarrow} l}{\langle cont \: x,\: s \rangle \stackrel{\text{eval}}{_\rightsquigarrow} v} \text{ , where } lookup^\mathcal{A}(s,l)=v.\]Execution of Commands
Execution of commands is characterized using another relation, \(\stackrel{\text{exec}}{_\rightsquigarrow}\), axiomatized in a manner similar to \(\stackrel{\text{eval}}{_\rightsquigarrow}\).
The first rule describes the execution of an assignment statement. In words, we execute $x:=M$ in store $s$ by evaluating $M$ and then updating $s$ so that location $x$ now contains this value.
\[\frac{\langle M,\: s \rangle \stackrel{\text{eval}}{_\rightsquigarrow} v}{\langle x:=M,\: s \rangle \stackrel{\text{exec}}{_\rightsquigarrow} s'} \text{ , where } update^\mathcal{A}(s,\eta(x),v)=s'.\]The remaining rules explain the execution of compound programs using the results of executing their parts.
It is worth mentioning that the execution relation defined here represents complete execution. If \(\langle P,\: s \rangle \stackrel{\text{eval}}{_\rightsquigarrow} s'\), then this is to be understood as meaning that if we start executing $P$ with store $s$, we will eventually halt with store $s’$.
Of course, you can also axiomatize this in a single-execution-step manner.
Sequencing and conditional are not very complicated. To execute $P_1; P_2$, we “first” execute $P_1$, and then execute $P_2$ in the resulting store.
\[\frac{\langle P_1,\: s \rangle \stackrel{\text{exec}}{_\rightsquigarrow} s',\: \langle P_2,\: s \rangle \stackrel{\text{exec}}{_\rightsquigarrow} s''}{\langle P_1;P_2,\:s \rangle \stackrel{\text{exec}}{_\rightsquigarrow} s''}\]For $\text{if } B \text{ then } P_1 \text{ else } P_2$, we evaluate $B$ and then execute $P_1$ or $P_2$ accordingly. It takes two inference rules to express this, one for the case when $B$ evaluates to $true$ and the other for $false$.
\[\frac{\langle B,\: s \rangle \stackrel{\text{eval}}{_\rightsquigarrow} true,\: \langle P_1,\: s \rangle \stackrel{\text{exec}}{_\rightsquigarrow} s'}{\langle \text{if } B \text{ then } P_1 \text{ else } P_2, \:s \rangle \stackrel{\text{exec}}{_\rightsquigarrow} s'}\] \[\frac{\langle B,\: s \rangle \stackrel{\text{eval}}{_\rightsquigarrow} false,\: \langle P_2,\: s \rangle \stackrel{\text{exec}}{_\rightsquigarrow} s'}{\langle \text{if } B \text{ then } P_1 \text{ else } P_2, \:s \rangle \stackrel{\text{exec}}{_\rightsquigarrow} s'}\]There are two rules for $\text{while } B \text{ do } P \text{ od}$. The first takes care of the case when $B$ evaluates to $false$. The second rule “says” that when $B$ is true, we execute $\text{while } B \text{ do } P \text{ od}$ by first executing $P$, and then executing $\text{while } B \text{ do } P \text{ od}$ in the resulting store.
\[\frac{\langle B,\: s \rangle \stackrel{\text{eval}}{_\rightsquigarrow} false}{\langle \text{while } B \text{ do } P \text{ od}, \:s \rangle \stackrel{\text{exec}}{_\rightsquigarrow} s}\] \[\frac{\langle B,\: s \rangle \stackrel{\text{eval}}{_\rightsquigarrow} true,\: \langle P,\: s \rangle \stackrel{\text{exec}}{_\rightsquigarrow} s',\: \langle \text{while } B \text{ do } P \text{ od}, \:s' \rangle \stackrel{\text{exec}}{_\rightsquigarrow} s''}{\langle \text{while } B \text{ do } P \text{ od}, \:s \rangle \stackrel{\text{exec}}{_\rightsquigarrow} s''}\]The second rule may be slightly unsettling, since it might appear that we are defining the execution of a $\text{while}$ loop in terms of itself. However, this set of rules is not intended to be a definition of $\stackrel{\text{exec}}{_\rightsquigarrow}$ by induction on the structure of formulas. (That would be a denotational semantics.)Instead, this is an inference rule telling us some fact about execution. This fact has a computational interpretation, since we may read the rule as a list of instructions for executing $\text{while } B \text{ do } P \text{ od}$.
To get some feel for how the rules work, it is best to work an example.
Example
In this section, we will work out the execution of a simple predecessor program that sets $p$ to $n-1$, using a “scratch” variable $m$.
We let \(m:loc ,\: p:loc ,\: n:val\). We assume that $val$ is the type of natural numbers, and that $p$ and $m$ denote different locations. Under these assumptions, we may write the following program to compute predecessor.
\[\begin{split} &p := 0;\\ &m := 0;\\ &\text{while } (cont \: m) \neq n \text{ do}\\ & \quad \quad p := cont \: m;\\ & \quad \quad m := (cont\: m) + 1;\\ & \text{od} \end{split}\]For concreteness, let us assume that the value of $n$ is $3$, and write $l_p$ and $l_m$ for locations $\eta(p)$ and $\eta(m)$, respectively. Since we will use this fact repeatedly, we begin by noting that in any store $s$, we have \(\langle p,\: s \rangle \stackrel{\text{eval}}{_\rightsquigarrow} l_p\) and \(\langle m,\: s \rangle \stackrel{\text{eval}}{_\rightsquigarrow} l_m\).
If we use the symbol $P$ for the entire program above, our goal is to construct a proof of an assertion \(\langle P,\: s \rangle \stackrel{\text{exec}}{_\rightsquigarrow} s'\) using the axioms and inference rules of the operational semantics.
Since $P$ initializes all of its assignable variables, it does not matter what the initial store $s$ is. In attempting to find a proof, we will discover the unique store $s’$ for which \(\langle P,\: s \rangle \stackrel{\text{exec}}{_\rightsquigarrow} s'\) is provable. We proceed by selecting an inference rule whose conclusion matches the form of $P$, and continue by reading inference rules from the bottom up.
Since program $P$ has the form \(p:=0;\: Q\), we look at the sequence rule. If we execute \(\langle p:=0,\: s \rangle\), the result is \(s_1 = update \: s \: l_p \: 0\). We must now execute the remaining program with store $s_1$. Since the next statement is also an assignment, similar reasoning applies, and so it remains to execute the $\text{while}$ loop from store $s_2$ with \(lookup \: s_2 \: l_m = lookup \: s_2 \: l_p = 0\).
We determine which $\text{while}$ inference rule applies by evaluating the boolean test. Since
\[\langle(cont \: m) \neq n,\: s_2 \rangle \stackrel{\text{eval}}{_\rightsquigarrow} true,\]we must use the second inference rule for $\text{while}$. This rule requires us to determine both the store obtained by executing the loop body, and the result of executing the entire $\text{while}$ statement in this store. It is not hard to see that
\[\langle p := cont \: m; \:m := (cont\: m) + 1 ,\: s_2 \rangle \stackrel{\text{exec}}{_\rightsquigarrow} s_3\]where \(lookup \: s_3 \: l_p =0\) and \(lookup \: s_3 \: l_m = 1\). We then test the boolean expression and find
\[\langle(cont \: m) \neq n,\: s_3 \rangle \stackrel{\text{eval}}{_\rightsquigarrow} true,\]which leads us to calculate
\[\langle p := cont \: m; \:m := (cont\: m) + 1 ,\: s_3 \rangle \stackrel{\text{exec}}{_\rightsquigarrow} s_4\]where \(lookup \: s_4 \: l_p =1\) and \(lookup \: s_4 \: l_m = 2\). Repeating the body again, we get
\[\langle(cont \: m) \neq n,\: s_4 \rangle \stackrel{\text{eval}}{_\rightsquigarrow} true,\] \[\langle p := cont \: m; \:m := (cont\: m) + 1 ,\: s_4 \rangle \stackrel{\text{exec}}{_\rightsquigarrow} s_5\]where \(lookup \: s_5 \: l_p =2\) and \(lookup \: s_5 \: l_m = 3\). It is easy to see that
\[\langle(cont \: m) \neq n,\: s_5 \rangle \stackrel{\text{eval}}{_\rightsquigarrow} false,\]so finally we have reached a store where the loop test fails. At this point, we can construct a proof that execution of the entire program $P$ from store $s$ terminates in store $s_5$. The way to write this proof down is simply to combine the assertions about evaluation and execution above using the inference rules for $\text{while}$ loops.