Variables and the assignment instruction

The variables which we have been using in the functional model (e.g., $n,a,b,count$ etc.) have no special meaning other than that they can be instantiated with values of a given type. These variables are similar to those used in algebra. In contrast, in the imperative model we will use variables to store the state of a computation. In this model, a ``declaration'' of variables to be of a certain type with a statement like

int a,b;

creates and reserves two locations (or boxes) with the names $a$ and $b$ in which integer values can be stored.

Initially, immediately after the declaration, the contents of the boxes with names $a$ and $b$ are undefined. The following assignment instruction stores the integer 2 in the location named $a$

a = 2;

The above is read as ``$a$ assigned 2''. The content of the location $b$ is still undefined and the state of the variables is

A subsequent assignment instruction of the form

b = a;

changes the state to

Note that the content of $a$ gets copied to $b$, and $a$ is unchanged. A further assignment instruction

a = a + b;

changes the state to:

The contents of $a$ gets replaced by the sum of the present contents of $a$ and $b$, whereas the contents of $b$ remains unchanged.

On the left of the $=$ operator must be a single variable whose state is being updated, and on the right must be an expression comprising operators, variables and values. The right side must evaluate to the same type as the variable specified in the left.

As a result of this, in the imperative style, state changes can be performed only one at a time. Consequently, simultaneous changes in the values of several variables have to be performed in some orderly fashion, one-at-a time, so as to ensure that the desired final state is obtained through several one-step changes.

The state of the computation at any instant is a snapshot of the contents of all the variables used in the algorithm.

As an example of an imperative style algorithm using the assignment instruction, let us consider the following problem of swapping the contents of two variables.

Example 4.1   Exchanging the values of two variables $a$ and $b$ (swapping).
Given the initial state of two variables $a$ and $b$ of the same type, we have to construct an algorithm to exchange their values (contents). Assuming that the initial contents of $a$ and $b$ are $a0$ and $b0$ respectively, we can describe the initial and the final states as

$$(a = a0) \wedge (b = b0)$$

$$(a = b0) \wedge (b = a0)$$

The `pre-condition' and the `post-condition' are logical properties of the initial and the desired final states of the computation respectively. Together they form the specification for the algorithm. Thus the objective of the algorithm is to change the state of the computation, through a sequence of steps, so that finally the post-condition is true given that the pre-condition is true to start with. We can achieve the transformation by using a variable $temp$ for temporary storage. We can first copy the contents of $a$ to $temp$, then replace the contents of $a$ with the contents of $b$, and finally replace the content of $b$ with that of $temp$. We describe the complete imperative algorithm as

/* assert $A:$ $(a = a0) \wedge (b = b0)$ */

temp = a;
a = b;
b = temp;

/* assert $B:$ $(a = b0) \wedge (b = a0)$ */

In the above example, the three assignment instructions have to be executed in the given order to achieve the exchange. An algorithm in the imperative model is a sequence of instructions which have to be executed in a step by step manner to carry out a desired computation. The instructions are separated by the symbol `;'. The sequence of three instructions may be regarded as a single compound instruction. To enable us to regard certain sequences of instructions as a single instruction we use a bracketing mechanism, where the left bracket is the symbol { and the closing bracket is the symbol }. Hence the above algorithm could be rewritten using brackets as follows

/* assert $A:$ $(a = a0) \wedge (b = b0)$ */

{
   temp = a;
   a = b;
   b = temp;
}

/* assert $B:$ $(a = b0) \wedge (b = a0)$ */

As we will see the {...} brackets are very useful to avoid possible confusion.