# 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._

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._

//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._

//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.