Simple Immutable-Variable Programs
Immutable variables are declared by means of the keyword
They are particularly easy to reason about.
We consider two problems that we commonly encounter in programming:
- Programs that yield a wrong result
- Programs that abort because undefined behaviour
Debugging a Simple Fragment: Wrong Result
Let’s consider the following very simple program fragment consisting of three immutable assignments.
1val x: Z = 1 2val y: Z = x + x + 1 3val z: Z = x + y
We can easily determine the values of the variables
z at the different locations in the fragment:
Executing line 1 assigns
x the value
executing line 2 assigns
y the value
3 because the value of
executing line 3 assigns
z the value
4 because the value of
1 and the value of
We perform this type of step-by-step “mental evaluation”, reasoning the value of each variable assignment, if we want to find an error in a program.
For instance, if we expect the value of
z above to be
3 after execution of line 3,
then somewhere on the way of our mental execution we ought to be able to observe an “unexpected value”.
We can make our expectations about the evaluation more explicit by inserting
assert statements into the program.
assert statement does nothing
if the condition stated as its parameter is true when the statement is executed – execution just continues past the assertion.
Otherwise, execution is aborted. This gives us a concise means to express “continue program execution if my expectations about the program’s meaning are correct; otherwise halt where my expectations are violated”, e.g., so we can diagnose and fix the problem.
The following fragment aborts at line 4.
1val x: Z = 1 2val y: Z = x + x + 1 3val z: Z = x + y 4assert(z == 3)
We observe, that the assigment to variable
z is wrong. (John: According to the assert statement, we expected the value of z to be 3, but we executed the program and the assertion failed with a message that z actually has the value 4.)
Suppose, taking the sum
x + y is intended. (John: suppose calculating the value of
z as the sum
x + y is intended, thus the assignment to
z is correct, but we must have made a mistake before that.)
Thus, we need to have a look at the values of
Further suppose, the value of
x should be
1. (John: Our intentions at this point are that
x should have the value of
y the value of
Then the value of
y must be
Let’s insert a corresponding
assert statements into the fragment to express our intentions.
1val x: Z = 1 2val y: Z = x + x + 1 3assert(x == 1) 4assert(y == 2) 5val z: Z = x + y 6assert(z == 3)
(John: explain that the assertion for x succeeds but the one for y fails.)
We conclude that the assigment to
y must be wrong (because we have determined that everything else is fine).
We know that the value of
x must be
1 when the assignment to
y is executed.
To fix the error we have to change the assignment to
y like shown below, for instance.
1val x: Z = 1 2assert(x == 1) 3val y: Z = x + 1 4assert(x == 1) 5assert(y == 2) 6val z: Z = x + y 7assert(z == 3)
(John: when running the program, all assertions succeed, and thus we know that … )
This program assigns value
3 to variable
We have approached the faulty fragment by a method of program debugging:
We have stated which result we expected and
then traced values of variables occuring during the execution of the fragment
until we have found the error, e.g, the erroneous assigment to variable
Note, that we have traced values forwards following the sequence of assigments
but that have stated the expected values backwards starting from the result.
This is a rather natural way to approach reasoning about programs
as the information about the expected values propagates backwards from the result
and the information about values propagates forward along the executed assignments.
There is one serious problem with the approach we have just followed.
We should have been explicit about the expected result
z == 3 of the fragment from the beginning of our coding activity.
That is, we should have started with the second fragment (of which we state the fixed version below).
1val x: Z = 1 2val y: Z = x + 1 3val z: Z = x + y 4assert(z == 3)
We shall do this systematically from now on. As we go on, we’ll use additional techniques to specify expected results that offer better support for reasoning.
(John: it seems like we should use phrases above like “We state our intentions/expectations” and also “we consider the facts that must be true at/after each statement in the program”, and “when we try to reason about whether the assertion holds or not, we see if the facts at that point will cause the assertion to be true”.)
We’ll also introduce techniques to specify expected input of a program. The following section provides a small example to motivate this.
Debugging a Simple Fragment: Undefined Behaviour
Consider the following program fragment.
The assignment to
z aborts because division by zero is undefined.
That is, before the assignment is executed we expect the condition
y != 0 to hold.
1val x: Z = 2 2val y: Z = 0 3val z: Z = x / y 4assert(z == 2)
Let’s insert the corresponding
1val x: Z = 2 2val y: Z = 0 3assert(y != 0) 4val z: Z = x / y 5assert(z == 2)
y != 0 no longer refers to a specific value of variable
y. That is, for the assertion to pass,
y may be any value from the set of integers that are not
0. In terms of our desire for a successful program execution, the assertion describes the set of values for which
x / y is defined.
y != 0 is a fact that we need to establish before evaluting
x / y.
Now, we can trace the value of
y and check whether it satisfies the fact
y != 0.
Performing our mental execution of the program, we see that variable
y is assigned the value
Let’s insert a corresponding assertion to capture our knowledge about the value of
y at that point.
1val x: Z = 2 2val y: Z = 0 3assert(y == 0) 4assert(y != 0) 5val z: Z = x / y 6assert(z == 2)
y == 0 (line 3), we can substitute
y in the condition
y != 0, obtaining
0 != 0.
Of course, this is false, and for this reason the program aborts when evaluating
assert(y != 0).
If we change the value assigned to
2, we get the following fragment.
1val x: Z = 2 2val y: Z = 2 3assert(y == 2) 4assert(y != 0) 5val z: Z = x / y 6assert(z == 2)
Evaluation succeeds for the assignment to
x / y is defined for
y == 2.
Of course, the fragment still does not yield
z == 2, and so the last assertion fails. If we change the program so that variable
y is assigned the value
1, then the entire fragment executes without a run-time exception or assertion violation.
1val x: Z = 2 2val y: Z = 1 3assert(y == 1) 4assert(y != 0) 5val z: Z = x / y 6assert(z == 2)
In larger programs it becomes virtually impossible to keep in your head all the conditions and values
that need to be traced and satisfied during a mental execution of a program.
This is where software tools like Logika intervene.
Logika provides support for this tracing and
the derivation of new facts to manage the scale and complexity associated with reasoning about programs.
We will see that such tools are most effective if we introduce some additional contracts focus solely on specification and automated reasoning. Some of these constructs are unlike
assert in that they are not executable (they are simply ignored during execution) and their entire purpose is to support reasoning (both mental and automated).
assert statement remains useful for purposes linked to the execution of programs:
- We can use it to check runtime conditions in programs for faults beyond our control like random hardware faults. We will not follow up on this here. Our focus is on reasoning and those aspects that are under our control.
- We can use it or specialised variants for software testing. Software testing is closely related to reasoning about software programs in the way outlined above. Tracing values and relating them to facts provides valuable information for the creation of test cases.
We have seen above that facts are used to specify conditions for defined behaviour (John: avoided run-time exceptions?), e.g., using an assertion, we stated that we needed the fact
y != 0 to hold before a division operation to avoid the operation throwing a run-time exception.
But we haven’t used them for more yet.
Consider the following fragment (where function
randomInt yields some arbitrary integer value)
val m: Z = randomInt() val n: Z = randomInt() val z: Z = m + n val y: Z = z - n val x: Z = z - y assert(x == n & y == m)
Can we still determine whether the assertion at the end holds even though we don’t know the values of
Let’s trace the facts established by the assignments to the variables
z through the fragment,
and derive new facts by algebraic reasoning using laws of integer arithmetic.
- After the assignment to
zin line 3, we obtain the fact
z == m + n. This is just what the assignment says.
- After the assignment to
yin line 4, we obtain additionally
y == z - n. Using the equation
z == m + nthat still holds after the assignment to
y, we can derive a new fact, namely,
y == (m + n) - nby substituting
m + nfor
y == z - n. We can simplify
y == (m + n) - nto
y == m + (n - n)and further to
y == m.
- After the assignment to
xin line 5, we obtain
x == z - yas a new fact. We can make use of the two facts
z == m + nand
y == mthat remain true after the assignment to
x. We can substitute
x == z - yto obtain
x == (m + n) - mwhich we can simplify to
x == n.
- Finally, we have two facts
x == nand
y == m. So, we can conclude
x == n & y == mand the assertion in line 6 must always be true, independently of the values of
Note that because we didn’t make any assumptions about the values of
n, we have demonstrated (i.e., proved) that the assertion holds for all possible values of
We are so confident in our reasoning that we might now view the use of the
assert statement in line 6 appear redundant (we have clearly demonstrated that the assertion will always succeed).
As we shift our perspective from execution to the proof-based reasoning illustrated above, we introduce some alternate notation to indicate the facts that we know to be true via our proof-based reasoning. We’ll use special proof notation instead of
assert and intersperse proof information
supporting reasoning such as just presented in the program text.
Instead of the verbose reasoning narrative written out above, our new notation lets us state the proof more concisely by noting the most important facts as series of deductions as comments in the program fragment. We know how to read it according to our reasoning narrative above. An additional advantage of the short form is that one can grasp quickly the important steps and facts of a proof.
val m: Z = randomInt() val n: Z = randomInt() val z: Z = m + n // deduce z == m + n val y: Z = z - n // deduce y == z - n // deduce y == (m + n) - n // deduce y == m val x: Z = z - y // deduce x == z - y // deduce x == (m + n) - m // deduce x == n // deduce x == n & y == m assert(x == n & y == m)