Assignment Statements

Assignment statements in a program come in two forms – with and without mutations. Assignments without mutation are those that give a value to a variable without using the old value of that variable. Assignments with mutation are variable assignments that use the old value of a variable to calculate a value for the variable.

For example, an increment statement like x = x + 1 MUTATES the value of x by updating its value to be one bigger than it was before. In order to make sense of such a statement, we need to know the previous value of x.

In contrast, a statement like y = x + 1 assigns to y one more than the value in x. We do not need to know the previous value of y, as we are not using it in the assignment statement. (We do need to know the value of x).

Assignments without mutation

We have already seen the steps necessary to process assignment statements that do not involve variable mutation. Recall that we can declare as a premise any assignment statement or claim from a previous logic block involving variables that have not since changed.

For example, suppose we want to verify the following program so the assert statement at the end will hold:

import org.sireum.logika._

val x: Z = 4

val y: Z = x + 2

val z: Z = 10 - x

//the assert will not hold yet
assert(y == z & y == 6)

Since none of the statements involve variable mutation, we can do the verification in a single logic block:

import org.sireum.logika._

val x: Z = 4    

val y: Z = x + 2

val z: Z = 10 - x

l"""{
    1. x == 4               premise     //assignment of unchanged variable
    2. y == x + 2           premise     //assignment of unchanged variable
    3. z == 10 - x          premise     //assignment of unchanged variable
    4. y == 4 + 2           subst1 1 2
    5. z == 10 - 4          subst1 1 3
    6. y == 6               algebra 4
    7. z == 6               algebra 5
    8. y == z               subst2 7 6
    9. y == z ∧ y == 6      ∧i 8 6
}"""

//now the assert will hold
assert(y == z & y == 6)

Note that we did need to do ∧i so that the last claim was y == z ∧ y == 6 , even though we had previously established the claims y == z and y == 6. In order for an assert to hold (at least until we switch Logika modes in chapter 10), we need to have established EXACTLY the claim in the assert in a previous logic block.

Assignments with mutation

Assignments with mutation are trickier – we need to know the old value of a variable in order to reason about its new value. For example, if we have the following program:

import org.sireum.logika._

var x: Z = 4

x = x + 1

//this assert will not hold yet
assert(x == 5)

Then we might try to add the following logic blocks:

import org.sireum.logika._

var x: Z = 4

l"""{
    1. x == 4               premise     //from previous variable assignment
}"""

x = x + 1

l"""{
    1. x == x + 1           premise     //NO! Need to distinguish between old x (right side) and new x (left side)
    2. x == 4               premise     //NO! x has changed since this claim

}"""

//this assert will not hold yet
assert(x == 5)

…but then we get stuck in the second logic block. There, x is supposed to refer to the CURRENT value of x (after being incremented), but both our attempted claims are untrue. The current value of x is not one more than itself (this makes no sense!), and we can tell from reading the code that x is now 5, not 4.

To help reason about changing variables, Logika has a special name_old value that refers to the OLD value of a variable called name, just before the latest update. In the example above, we can use x_old in the second logic block to refer to x’s value just before it was incremented. We can now change our premises and finish the verification as follows:

import org.sireum.logika._

var x: Z = 4

l"""{
    1. x == 4               premise     //from previous variable assignment
}"""

x = x + 1

l"""{
    1. x == x_old + 1       premise     //Yes! x equals its old value plus 1
    2. x_old == 4           premise     //Yes! The old value of x was 4
    3. x == 4 + 1           subst1 2 1  
    4. x == 5               algebra 3   //Could have skipped line 3 and used "algebra 1 2" instead
}"""

//now the assert will hold
assert(x == 5)

By the end of the logic block following a variable mutation, we need to express everything we know about the variable’s current value WITHOUT using the _old terminology, as its scope will end when the logic block ends. Moreover, we only ever have one _old value available in a logic block – the variable that was most recently changed. This means we will need logic blocks after each variable mutation to process the changes to any related facts.

Variable swap example

Suppose we have the following Logika program:

import org.sireum.logika._

var x: Z = readInt()
var y: Z = readInt()

val temp: Z = x
x = y
y = temp

//what do we want to assert we did?

We can see that this program gets two user input values, x and y, and then swaps their values. So if x was originally 4 and y was originally 6, then at the end of the program x would be 6 and y would be 4.

We would like to be able to assert what we did – that x now has the original value from y, and that y now has the original value from x. To do this, we might invent dummy constants called xOrig and yOrig that represent the original values of those variables. Then we can add our assert:

import org.sireum.logika._

var x: Z = readInt()
var y: Z = readInt()

//the original values of both inputs
val xOrig: Z = x
val yOrig: Z = y

val temp: Z = x
x = y
y = temp

//x and y have swapped
//x has y's original value, and y has x's original value
assert(x == yOrig & y == xOrig)     //this assert will not yet hold

We can complete the verification by adding logic blocks after assignment statements, being careful to update all we know (without using the _old value) by the end of each block:

import org.sireum.logika._

var x: Z = readInt()
var y: Z = readInt()

//the original values of both inputs
val xOrig: Z = x
val yOrig: Z = y

l"""{
    1. xOrig == x           premise
    2. yOrig == y           premise
}"""

//swap x and y
val temp: Z = x
x = y
l"""{
    1. x == y                   premise     //from the assignment statement
    2. temp == x_old            premise     //temp equaled the OLD value of x
    3. xOrig == x_old           premise     //xOrig equaled the OLD value of x
    4. yOrig == y               premise     //yOrig still equals y
    5. temp == xOrig            algebra 2 3
    6. x == yOrig               algebra 1 4
}"""
y = temp
l"""{
    1. y == temp                premise     //from the assignment statement
    2. temp == xOrig            premise     //from the previous logic block (temp and xOrig are unchanged since then)
    3. yOrig == y_old           premise     //yOrig equaled the OLD value of y
    4. y == xOrig               algebra 1 2
    5. x == yOrig               premise     //from the previous logic block (x and yOrig are unchanged since then)
    6. x == yOrig ^ y == xOrig  ^i 5 4
}"""

//x and y have swapped
//x has y's original value, and y has x's original value
assert(x == yOrig & y == xOrig)     //this assert will hold now

Notice that in each logic block, we express as much as we can about all variables/values in the program. In the first logic block, even though xOrig and yOrig were not used in the previous assignment statement, we still expressed how the current values our other variables compared to xOrig and yOrig. It helps to think about what you are trying to claim in the final assert – since our assert involved xOrig and yOrig, we needed to relate the current values of our variables to those values as we progressed through the program.