Simple Mutable-Variable Programs
Mutable variables are declared by means of the keyword
Reasoning about mutable variables is much more complicated than reasoning about immutable variables.
The problem of dealing with undefined behaviour is not affected by this (John: maybe have this as a footnote, or state it later in an assessment. It seems to disrupt the flow of the explanation when written at this point).
Let’s have a look at a simple program using mutable variables.
Tracing Values and Facts
The following program swaps the values of two integer variables
y using simple arithmetic manipulations.
1// consider some example input values 2// represented using values for m and n 3val m: Z = 1 4val n: Z = 2 5// initialize the program variables x and y 6var x: Z = m 7var y: Z = n 8// carry out computation to achieve swap 9x = x + y 10y = x - y 11x = x - y 12// check condition indicating that swap has been achieved 13assert(x == 2 & y == 1)
We can verify this in two ways. In the first way, illustrated above, we use some arbitrary concrete values
n we then we can trace the values through the program. We first assign
Then, at the end of the program, we can conclude that the program swaps the values of two integer variables
if the values of
y are now
1, respectively. A summary of our mental execution is as follows: in line 9 variable
x is assigned
2; in line 10 variable
y is assigned
and in line 11 variable
x is assigned
This is what we do if we are testing a program: we choose some appropriate concrete inputs, we execute a program/method, and afterwards we check that the actual result of the program corresponds to a stated expected result.
From Values to Facts
Alternatively, instead of reasoning about specific concrete values, we can consider arbitrary values and trace facts about the variables through the program to construct a proof to that the expected result (
x == n & y == m) holds at the end.
1// consider arbitrary input values 2// represented by random values for m and n 3val m: Z = randomInt() 4val n: Z = randomInt() 5// initialize the program variables x and y 6var x: Z = m 7var y: Z = n 8// carry out computation to achieve swap 9x = x + y 10y = x - y 11x = x - y 12// check condition indicating that swap has been achieved 13assert(x == n & y == m)
The following narrative summarizes our reasoning (fact tracing) about the program:
- After executing line 6 we obtain the new fact
x == m.
- After executing line 7 we obtain the additional fact
y == n.
Now we have established symbolically the initial values of the variables. Let’s follow up the evolution of the facts as we proceed through the computation.
- After executing line 9 we obtain
x == x + y. Something is wrong here!
- If we have
x == mand
x == x + y, we can infer that
- The problem we see here is that in an assignment
x = x + ythe
xon the left-hand side refers to the new value of variable
x, and the value on the right-hand side refers to the old value of variable
x. Of course, we know this. But we also need to reflect this formally in the way we reason about programs.
- Distinguishing old facts from new facts
- The solution the problem we have just encountered to rename variables from old facts systematically, so that we can distinguish old facts about a variable from newly established facts. The facts related to variables evolve during program execution. Renaming variables permits us to see the past evolution of the facts concerning a variable.
- After execution of line 9, variable
xas used in line 6 needs to be renamed. To keep matters simple, let’s just use a counter to determine when the variable is assigned: the term
At(x,0)describes the “new”
xin line 6. We postulate
At(x,0) = mand use
At(x,0)thereafter to refer to that
x. Thus, the old fact
x == mbecomes
At(x,0) = m. The assignment in line 9 then establishes
At(x,1) == At(x,0) + At(y,0): the terms
At(y,0)on the right-hand side refers to variables
y“from the past”. We can proceed like this to complete the proof continuing to rename variables as we encounter assignments to them.
For ease of reference we annotate the program fragment with comments detailing the introduction of terms
representing past assignments to variables.
Note, that the “latest”
y are left untouched
because there are no conflicting “newer” uses of
1// consider arbitrary input values 2// represented by random values for m and n 3val m: Z = randomInt() 4val n: Z = randomInt() 5// initialize the program variables x and y 6var x: Z = m // At(x,0) 7var y: Z = n // At(y,0) 8// carry out computation to achieve swap 9x = x + y // At(x,1) 10y = x - y // y 11x = x - y // x 12// check condition indicating that swap has been achieved 13assert(x == n & y == m) // refers to the "current" x and y
- After executing line 9 we obtain
At(x,1) == At(x,0) + At(y,0); keeping the old fact
At(x,0) == m. We also know
At(y,0) == nfrom the first assignment to
yin line 7. Thus, we can infer
At(x,1) == m + n.
- After executing line 10 we obtain
y == At(x,1) - At(y,0)(refering to the old
yon the right-hand side). The old facts
At(y,0) == nand
At(x,1) == m + nare preserved. Thus we can infer
y == (m + n) - n, and by calculation
y == m.
- After executing line 11 we obtain
x == At(x,1) - y; and
At(x,1) == m + nfrom before. We infer
x == (m + n) - y, and further
x == (m + n) - nbecause
y == m. Thus, we have
x == n.
- Hence, after excuting lines, 9, 10, and 11 we have
x == nand
y == m, in other words
x == n & y == m.
As before we can state the proof more concisely as a series of deductions in the comments. We have not mentioned the renamed variables in proof. They can make a proof rather difficult to read. Instead, we have deduced facts that make mention or reference of older unnecessary. This helps for reading the proof: we have only to look only at the most recent assignment before the one currently considered to derive new facts.
1// initialise variables 2val m: Z = 1 3val n: Z = 2 4var x: Z = m 5// deduce x == m 6var y: Z = n 7// deduce y == n 8// carry out computation 9x = x + y 10// deduce x == m + n 11y = x - y 12// deduce y == (m + n) - n 13// deduce y == m 14x = x - y 15// deduce x == (m + n) - m 16// deduce x == n 17// deduce x == n & y == m 18// check condition 19assert(x == n & y == m)
In the preceding section we can see that reasoning about program becomes rather intricate quickly. Partly this is caused by assignments to variables, but the amount of detail and relationships between different variables to consider increases fast in software programs. Even small programs become quickly rather difficult to handle. For this reason, we use software to assist with this reasoning such as Logika. With Logika we can also master large programs because of the software tracks facts and carries out renaming automatically. Additional concepts and techniques we encounter later provide the necessary toolset to scale the approach to large programs containing common programming constructs such as while loops.