Mutable variables are declared by means of the keyword var. 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 x and 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 1 and 2 for m and n we then we can trace the values through the program. We first assign m (1) to x and n (2) to y Then, at the end of the program, we can conclude that the program swaps the values of two integer variables if the values of x and y are now 2 and 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 1; and in line 11 variable x is assigned 1. 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.

First Attempt

  • After executing line 9 we obtain x == x + y. Something is wrong here!
  • If we have x == m and x == x + y, we can infer that y must equal 0.
  • The problem we see here is that in an assignment x = x + y the x on 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 x as 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” x in line 6. We postulate At(x,0) = m and use At(x,0) thereafter to refer to that x. Thus, the old fact x == m becomes At(x,0) = m. The assignment in line 9 then establishes At(x,1) == At(x,0) + At(y,0): the terms At(x,0) and At(y,0) on the right-hand side refers to variables x and y “from the past”. We can proceed like this to complete the proof continuing to rename variables as we encounter assignments to them.

Second Attempt

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” x and y are left untouched because there are no conflicting “newer” uses of x and y.

 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) == n from the first assignment to y in 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 y on the right-hand side). The old facts At(y,0) == n and At(x,1) == m + n are 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 + n from before. We infer x == (m + n) - y, and further x == (m + n) - n because y == m. Thus, we have x == n.
  • Hence, after excuting lines, 9, 10, and 11 we have x == n and y == m, in other words x == n & y == m.

Summary

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)

Program Intricacy

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.