The examples at the end of the previous chapter showed that assignment in
computer language is different from equality in algebra – in algebra,
`x = x + 1`

is a self-contradiction, whereas in computer language,
it is a new assertion, *cancelling a previously known one*.
In this chapter, we make precise the semantics of assignment for the knowledge
that travels through a computer program.

From the previous chapter, we know how to apply forwards-reasoning techniques to single-assignment programs:

```
var hours: Z = 4
l"""{ 1. hours == 4 premise // (generated by the assignment)
}"""
val minutes: Z = hours * 60
l"""{
1. hours == 4 premise // (the last-stated fact, unaltered)
2. minutes == hours * 60 premise // (the fact generated by the assignment)
3. minutes == 240 algebra 1 2
}"""
// here, we know that minutes == 240
// print hours, minutes
```

From now on, we enclose our logical and algebraic reasoning steps in set braces
to distinguish it from the text of the program.
We will number each reasoning step;
*premises* are facts that are generated by the assignment command or the
last-established fact prior to the assignment.
In Line 3 of the above example, *algebra*, like that in the previous chapter,
was applied to the facts in Lines 1 and 2 to deduce the result.
A fact is also called an *assertion*.

Since we use both assignments and equations, we use `==`

to denote algebraic
equality.

In languages like C and Python, a programmer can insert `assert`

commands into
the program script to *force* that a logical property holds true during the
execution:

```
var hours: Z = readInt("Type an int > 2: ")
assume (hours > 2)
// execution reaches here _only if_ the value assigned to hours is > 2
var minutes: Z = hours * 60
// here, we know that minutes > 120
// print hours, minutes
```

(Note: Our programming examples will be coded in Python. This helper function will be used a lot, and we take it for granted:

```
def readInt(message = "Type an int: ") :
"""readInt is a helper function that reads an int from the display.
parameter: message - a string, the input prompt; default is 'Type an int:'
returns an int, typed by the user"""
needInput = True
while needInput :
text = raw_input(message)
if text.isdigit() :
answer = int(text)
needInput = False
return answer
```

When the computer executes the program, it checks that the integer assigned to
`hours`

is indeed greater than 2.
If it is, execution proceeds; if it is not, the computer halts the program with
an *assert exception* (a.k.a., assertion violation).
We can use `assert`

in our analysis:

```
var hours: Z = readInt("Type an int > 2: ")
assume (hours > 2)
l"""{ 1. hours > 2 premise // (fact generated from the assert)
}"""
var minutes: Z = hours * 60
l"""{
1. hours > 2 premise
2. minutes == hours * 60 premise
3. minutes > 120 algebra 1 2
}"""
// THE GOAL, minutes > 120, IS SATISFIED
// print hours, minutes
```

As noted at the end of the previous chapter, when we violate single assignment, our reasoning goes wrong. Consider:

```
var hours: Z = 4
l"""{ 1. hours == 4 premise }"""
var minutes: Z = hours * 60
l"""{
1. hours == 4 premise
2. minutes == hours * 60 premise
}"""
hours = 5
l"""{
1. hours == 5 premise
2. minutes == hours * 60 ??? // (NO --- this fact is corrupted)
}"""
```

A first modification of our reasoning for an assignment, `x = e`

, says that
we must cancel all facts that mention the old value of `x`

.
For the example, we might deduce:

```
var hours: Z = 4
l"""{ 1. hours == 4 premise }"""
var minutes: Z = hours * 60
l"""{
1. hours == 4 premise
2. minutes == hours * 60 premise
3. minutes == 240 algebra 1 2
}"""
hours = 5
l"""{
1. hours == 5 premise
2. minutes == 240 premise
}"""
```

But this isn’t good enough. Consider:

```
var x: Z = readInt("Type an int > 0: ")
assume (x > 0)
l"""{ 1. x > 0 premise }"""
x = x + 1
l"""{
1. x == x + 1 ?? No.
// We want to prove that x > 1. How?
}"""
```

In the assignment, `x = x + 1`

, we must distinguish between the “old” value of
`x`

, which appears on the assignment’s right-hand side, and its “new” value,
which appears on its left-hand side.
With this distinction, we can reason correctly about `x`

.
Here is the example repeated, with the distinction made clear:

```
var x: Z = readInt("Type an int > 0: ")
assume (x > 0)
l"""{ 1. x > 0 premise }"""
x = x + 1
l"""{
1. x_old > 0 premise // (from the previously established fact)
2. x == x_old + 1 premise // (from the assignment)
3. x_old == x - 1 algebra 2
4. x - 1 > 0 subst1 3 1 // (we substitute the equality stated in Line 3 into Line 1)
5. x > 1 algebra 4 // (this last line, which must not mention x_old,
// can be carried forwards as a premise to subsequent commands)
}"""
// WE'VE PROVED THAT x > 1
```

When we have an assertion, `P`

, that holds true just before an assignment,
`x = e`

, we calculate the assertions after the assignment, in two stages:

- We assert that
`x = [x_old/x]e`

and also`[x_old/x]P`

. The notation,`[x_old/x]E`

, means that we substitute (replace) all occurrences of`x`

within expression`E`

by`x_old`

. - We next apply deductions, giving us a new assertion,
`Q`

, that does not mention`x_old`

. This assertion can be carried forwards as a premise for future deduction.

This is what we did in the earlier example – we deduced `x > 1`

, which we can
carry forwards.
We then forget all the assertions that mentioned `x_old`

.

The rule’s schematic looks likes this:

```
l"""{
...
m. P
}"""
x = e
l"""{
1. x == [x_old/x]e premise
2. [x_old/x]P premise
...
n. Q // (where Q must _not_ mention x_old)
}"""
```

Here is a second example that shows the form of reasoning we follow when working
with assignments.
Say that `y > x`

at the outset, and we wish to preserve this property as the
computation progresses.
We can prove it with algebra:

```
var x: Z = readInt()
var y: Z = readInt()
assume (y > x)
l"""{ 1. y > x premise }"""
x = x - 1
l"""{
1. y > x_old premise
2. x == x_old - 1 premise
3. x_old == x + 1 algebra 2 // This line abbreviates multiple small steps.
4. y > x + 1 subst1 3 1 // Substitute the equality on line 3 into the formula on line 1.
5. y > x algebra 4 // There is no mention of x_old
}"""
y = y + 1
l"""{
1. y_old > x premise
2. y == y_old + 1 premise
3. y > x algebra 1 2 // This line abbreviates these steps:
// y_old == y - 1
// y - 1 > x
// y > x + 1
}"""
```

After each command, a proof segment begins with the premises and then *subst*
and *algebra* steps lead to the last line, which states the knowledge that
travels forwards to the next command.
We must ensure that no “old” variables appear in the last line.

Here is a third example, where we wish to show that the value within variable
`x`

falls in a certain range (perhaps `x`

is used as an index to an array):

```
var x: Z = readInt()
// the precondition is that int x falls in the range, 1,2,...,99
assume (x > 0 & x < 100)
l"""{ 1. x > 0 ∧ x < 100 premise }"""
x = x + 1
l"""{
1. x_old > 0 ^ x_old < 100 premise
2. x_old > 0 ^e1 1
3. x == x_old + 1 premise
4. x_old + 1 > 1 algebra 2
5. x > 1 subst2 3 4
6. x_old < 100 ^e2 1
7. x_old + 1 < 101 algebra 6
8. x < 101 subst2 3 7
9. x > 1 ^ x < 101 ^i 5 8
}"""
// the postcondition is that x falls in the range, 2,3,...,100
```

The starting assertion about `x`

is sometimes called a *precondition*, because
it is the input property that the program requires to operate successfully.
The goal of the program is its *postcondition*.
The example uses new deduction laws that let us combine together and pull apart
assertions connected by `^`

(“and”).
There is also an explicit use of substitution (`subst`

), where the equality
substituted and the formula substituted into are both listed as line numbers.

Because our deductions often consist of multiple steps, it is convenient to use
the `^i`

law (“and-introduction”) to collect together the facts we wish to
carry forwards as premises for future use – from here on, we will carry
forwards only the *last line* of a proof as the premise for future use.
If we want to carry forwards multiple facts, we connect them together with
`^i`

.
Later, we use `^e`

(“and-elimination”) to extract the facts as needed.

Real-time controller software maintains *invariant properties* on the variables
it manipulates.
Here is a simplistic example: perhaps we build an electronic piggy bank, which
displays the value of the dimes inserted into it.
The bank’s controller software must maintain the relationship between the
quantity of dimes inserted in the bank and the dimes’ monetary value:

```
var dimes: Z = readInt()
var money: Z = dimes * 10
// the _invariant property_ is that money == dimes * 10 :
assert (money == dimes * 10)
l"""{ 1. money == dimes * 10 premise }"""
// Say that one more dime is inserted into the bank:
dimes = dimes + 1
l"""{
1. dimes == dimes_old + 1 premise
2. money == dimes_old * 10 premise
3. dimes_old == dimes - 1 algebra 1
4. money == (dimes - 1) * 10 subst1 3 2 // we use Lines 1 and 2 to eliminate dimes_old from the knowledge we have
}"""
// The amount of money is less that what it should be; we fix this:
money = money + 10
l"""{
1. money_old == (dimes - 1) * 10 premise
2. money == money_old + 10 premise
3. money_old == money - 10 algebra 2
4. money - 10 == (dimes - 1) * 10 subst1 3 1
5. money == dimes * 10 algebra 4
}"""
// The invariant property is restored: money == dimes * 10
```

The proof explains why we wrote the assignments that we did – we wanted to
maintain the logical property that `money == dimes * 10`

.

The above software is embedded in a chip within the piggy bank: when the child
inserts a dime, this activates the above code, which resets `dimes`

and
`money`

so that the invariant property is always holding true.
Then, when the values of `dimes`

and `money`

are displayed on the LED on the
side of the bank, their relationship, as stated by the invariant property, is
maintained.

Invariant properties are central to the development of real-time software, which iteratively monitors the values of input sensors and adjusts program variables so that invariants are maintained. This is the crucial concept within flight-control software, which uses inputs from a plane’s sensors to adjust rudders, joystick, and fuel intake so that a plane flies stably and on course.

The form of reasoning (invariant maintenance) just seen occurs automatically and unconsciously in seasoned programmers all the time, every time assignments are written. It plays a crucial role in object-oriented programming, where an object holds private variables and methods that maintain invariant properties of the private variables.

Sometimes we really must discuss the “old” value of a variable after an
assignment completes.
Here is a small but tricky program that swaps the values of the its two
variables, `x`

and `y`

:

```
var x: Z = readInt()
var y: Z = readInt()
val temp: Z = x
x = y
y = temp
// print x, y
```

At the end of the program, we want to assert that `y`

has `x`

’s value and
`x`

has `y`

’s.
To do this, we may invent dummy constants called `x_in`

and `y_in`

and
pretend they are the input values to `x`

and `y`

respectively:

```
val x_in: Z = readInt()
val y_in: Z = readInt()
var x: Z = x_in
var y: Z = y_in
l"""{
1. x == x_in premise
2. y == y_in premise
3. x == x_in ^ y == y_in ^i 1 2
}"""
val temp: Z = x
l"""{
1. temp == x premise
2. x == x_in ^ y == y_in premise
3. x == x_in ^e1 2
4. temp == x_in subst1 3 1
5. temp == x_in ^ (x == x_in ^ y == y_in) ^i 4 2
}"""
x = y
l"""{
1. x == y premise
2. temp == x_in ^ (x_old == x_in ^ y == y_in) premise
3. temp == x_in ^e1 2
4. x_old == x_in ^ y == y_in ^e2 2
5. y == y_in ^e2 4
6. x == y_in subst1 5 1
7. temp == x_in ^ y == y_in ^i 3 5
8. x == y_in ^ (temp == x_in ^ y == y_in) ^i 6 7
}"""
y = temp
l"""{
1. y = temp premise
2. x = y_in ^ (temp = x_in ^ y_old = y_in) premise
// . . . (you fill in the steps) . . .
4. y = x_in ^ x = y_in
}"""
// We've proved that x and y swapped their original values.
// print x, y
```

The dummy values `x_in`

and `y_in`

plus the assignment law navigate us
through the deduction.

After several examples, we are tempted to conclude that deducing forwards knowledge is a mechanical activity, where we do an assignment and then eliminate occurrences of the “old” variable, like this:

```
l"""{ P }"""
x = e
l"""{
1. [x_old/x]P premise
2. x == [x_old/x]e premise
// solve for x_old in terms of x and e :
3. x_old = ...x... algebra 2
// eliminate x_old in Line 1 :
4. [...x.../x_old]P subst1 3 1
}"""
```

We can apply this pattern to an earlier example – it works!

```
var x: Z = readInt()
assume (x > 0 & x < 100)
x = x + 1
l"""{
1. x_old > 0 ^ x_old < 100 premise
2. x == x_old + 1 premise
// Solve for x_old :
3. x_old == x - 1 algebra 2
// Eliminate x_old:
4. x - 1 > 0 ^ x - 1 < 100 subst1 3 1
}"""
// print x
```

One step of algebra gives us the desired goal that `x > 1`

and `x < 101`

.

Here is the piggy-bank example, which also works in this style:

```
var dimes: Z = readInt()
var money: Z = dimes * 10
assert (money == dimes * 10)
l"""{ 1. money == dimes * 10 premise }"""
dimes = dimes + 1
l"""{
1. dimes == dimes_old + 1 premise
2. money == dimes_old * 10 premise
3. dimes_old == dimes - 1 algebra 1 // Solve for dimes_old
4. money == (dimes - 1) * 10 subst1 3 2 // Eliminate dimes_old
}"""
money = money + 10
l"""{
1. money_old == (dimes - 1) * 10 premise
2. money == money_old + 10 premise
3. money_old == money - 10 algebra 2 // Solve for money_old
4. money - 10 == (dimes - 1) * 10 subst1 3 1 // Eliminate money_old
5. money == dimes * 10 algebra 4
}"""
// reprove the invariant, money == dimes * 10
// print dimes, money
```

Will the variable-elimination technique always lead us to the final goal? If so, perhaps we can write a proof generator that will automatically write the proofs for us!

Unfortunately, the answer here is “no”. The reason is that important intermediate knowledge can be lost, and here is a simple example that shows how:

```
var x: Z = readInt()
val y: Z = x * 2
l"""{ 1. y == x * 2 premise }"""
x = 3
l"""{
1. y == x_old * 2 premise
2. x == 3 premise
3. x_old == y / 2 algebra 1 // Solve for x_old
// We cannot eliminate x_old from Line 2 ?!
// The knowledge that travels forwards is only
// x == 3
// We lose knowledge about y.
}"""
val z: Z = 4
// prove here that y % 2 == 0, that is, y is an even-valued int
l"""{
1. x == 3 premise
2. z == 4 premise
// We cannot use x_old == y / 2 as a premise .... x_old has disappeared.
// Lines 1 and 2 cannot prove the goal.
}"""
```

A human sees how to repair the above proof – extract new knowledge about `y`

from premise `y == x_old * 2`

:

```
var x: Z = readInt()
val y: Z = x * 2
l"""{ 1. y == x * 2 premise }"""
x = 3
l"""{
1. y == x_old * 2 premise
2. y % 2 == 0 algebra 1 // because y is even-valued, even though
// we don't know what value it has
}"""
val z: Z = 4
// prove here that y % 2 == 0, that is, y is an even-valued int
l"""{ 1. y % 2 == 0 premise // DONE
}"""
```

When we analyze a program in a forwards direction, we work together with an automated checker tool to reach our goal.

The previous examples raise this question:
When we analyze a program from start to finish, which facts should we try to
deduce and carry forwards after each assignment?
We cannot answer this question unless we know the *goal assertion* we are trying
to prove at the program’s end.
For this reason, we should learn how to reason *backwards* from the goal at the
end of a program to the asserts at the beginning.
This is called *goal-directed reasoning*, and there is a simple, beautiful
deduction rule for assignments that takes the guesswork out of goal-directed
reasoning.

Here is an example.
Say that at program’s end, `x > 2`

must hold, and the program ends like this:

```
. . .
l"""{ subgoal: ??? }"""
x = y + 1
l"""{ goal: x > 2 }"""
```

What is the subgoal needed for success?
It appears that `y > 1`

must hold just before the assignment.
How did we calculate this?
Since the assignment “equates” `x`

with `y + 1`

, it must be `y + 1`

that
is greater than 2 – we *substitute* `y + 1`

into the goal, for `x`

,
that is, we compute the subgoal as:

```
[y + 1 / x] (x > 2) = (y + 1) > 2
```

that is, y > 1 is the subgoal:

```
. . .
l"""{ subgoal: y > 1 }"""
x = y + 1
l"""{ goal: x > 2 }"""
```

This reasoning is the basis of a “backwards law” for assignment commands.

The formal statement of the backwards-assignment law is this:

```
l"""{ subgoal: [e/x]G }"""
x = e
l"""{ goal: G }"""
```

The goal, `G`

, is sometimes called the assignment’s *postcondition*, and
the subgoal, `[e/x]G`

, is the *precondition*.
It is a formal, proved result that every such precondition, postcondition pair
calculated by the backwards-assignment law can be proved as a correct forwards
deduction with the forwards-assignment law.
Let’s use the backwards assignment law on an example from the previous section.

```
var x: Z = readInt()
assume (x > 0 & x < 100)
l"""{ ??? }"""
x = x + 1
l"""{ x > 1 ^ x < 101 (goal) }"""
// print x
```

The backwards assignment law tells us `???``

should be
`[x + 1/ x](x > 1 ^ x < 101)`

:

```
var x: Z = readInt()
assume (x > 0 & x < 100)
l"""{ x + 1 > 1 and x + 1 < 101 (subgoal) }"""
x = x + 1
l"""{ x > 1 ^ x < 101 (goal) }"""
// print x
```

Now, we use algebra to show that the assert proves the subgoal:

```
var x: Z = readInt()
assume (x > 0 & x < 100)
l"""{
1. x > 0 ^ x < 100 premise
2. x > 0 ^e1 1
3. x < 100 ^e2 1
4. x + 1 > 1 algebra 2
5. x + 1 < 101 algebra 3
6. x + 1 > 1 and x + 1 < 101 ^i 4 5 // (subgoal achieved)
}"""
x = x + 1
l"""{
1. x_old + 1 > 1 and x_old + 1 < 101 premise
2. x == x_old + 1 premise
3. x > 1 ^ x < 101 subst2 2 1 // (goal achived)
}"""
// print x
```

The backwards law helps us calculate exactly the correct knowledge at intermediate program points that will lead to the desired final goal.

This technique works well on programs that are sequences of assignments. Here are two examples from the previous section, reworked in backwards style:

```
var dimes: Z = readInt()
var money: Z = dimes * 10
assume WHAT??
dimes = dimes + 1
money = money + 10
// GOAL: money == dimes * 10
// print dimes, money
```

We fill in the subgoals one by one:

```
var dimes: Z = readInt()
var money: Z = dimes * 10
assume WHAT??
l"""{ SUBGOAL II: (money + 10) == (dimes + 1) * 10 }"""
dimes = dimes + 1
l"""{ SUBGOAL I: (money + 10) == dimes * 10 }"""
money = money + 10
// GOAL: money == dimes * 10
// print dimes, money
```

Some algebra simplifies the second subgoal into just `money == dimes * 10`

,
which must be asserted at the beginning.
Here is a previous problematic example, now neatly handled:

```
l"""{
ENTRY CONDITION: (x * 2) % 2 == 0 (which must always hold true!),
SO, true is the entry condition
}"""
y = x * 2
l"""{ SUBGOAL II: y % 2 == 0 (x doesn't matter!) }"""
x = 3
l"""{ SUBGOAL I: y % 2 == 0 (z doesn't matter!) }"""
z = 4
// GOAL: y % 2 == 0, that is, y is an even-valued int
```

The backwards technique works even when there is a self-referential assignment:

```
var x: Z = readInt()
assume (x > 1)
x = x + 1
l"""{ goal: x > 2 }"""
```

We calculate that the subgoal before the assignment must be
`[x + 1 / x](x > 2)`

, which is `(x + 1) > 2`

.
A small algebra step completes the forwards proof of the backwards deduction:

```
var x: Z = readInt()
assume (x > 1)
l"""{
1. x > 1 premise
2. x + 1 > 2 algebra 1
}"""
x = x + 1
l"""{
1. x = x_old + 1 premise
2. x_old + 1 > 2 premise
3. x > 2 subst2 1 2
}"""
```

By reasoning backwards, we avoid the need to work directly with `x_old`

–
the subgoals we calculate by substitution are correctly expressed in terms of
`x`

.
So, if your program has a clearly stated goal, you *can use backwards reasoning
to prove that the goal is achieved*.

To deduce the knowledge generated by a conditional (if-else) command, we must
analyze both arms (paths) within the command.
This is because some executions will follow the then-arm and some will follow
the else-arm.
Before we state the rules for forwards and backwards reasoning, we motivate the
key ideas with examples.
This conditional command sets `max`

to the larger of numbers `x`

and `y`

:

```
if (x > y) {
max = x
} else {
max = y
}
```

What can we assert when the command finishes, no matter what the values of `x`

and `y`

might be?
First, when we analyze the then-arm, we have:

```
max = x
l"""{ max == x }"""
```

and when we analyze the else-arm, we have:

```
max = y
l"""{ max == y }"""
```

These two deductions imply that, when the conditional finishes, one or the other property holds true:

```
if (x > y) {
max = x
} else {
max = y
}
l"""{ max == x v max == y }"""
```

This illustrates the first principle of conditional commands:
the knowledge producted by the command is the *disjunction* (or) of the
knowledge produced by each arm.
Later, we will learn how to apply cases analyses on disjunctive assertions to
extract useful knowledge.

Recall that the intent of the conditional was to set `max`

so that it holds
the larger of `x`

and `y`

.
The assertion we proved so far does not imply the desired goal.
This is because we ignored a critical feature of a conditional command:
*By asking a question — the test — the conditional command generates new
knowledge.*

For the then arm, we have the new knowledge that `x > y`

;
for the else-arm, we have that `~(x > y)`

, that is, `y >= x`

.
We can embed these assertions into the analysis of the conditional command,
like this, and conclude that, in both cases, `max`

holds the maximum of `x`

and `y`

:

```
val x: Z = readInt()
val y: Z = readInt()
var max: Z = readInt()
if (x > y) {
l"""{ 1. x > y premise }"""
max = x
l"""{
1. x > y premise
2. max == x premise
3. max >= x algebra 2
4. max >= y algebra 1 3
5. max >= x ^ max >= y ^i 3 4
}"""
} else {
l"""{
1. ~(x > y) premise
2. y >= x algebra 1
}"""
max = y
l"""{
1. max == y premise
2. y >= x premise
3. max >= y algebra 1
4. max >= x algebra 1 2
5. max >= x ^ max >= y ^i 4 3
}"""
}
l"""{ 1. max >= x ^ max >= y premise // (from the if-command)
}"""
```

Each arm generates the assertion that `max >= x ^ max >= y`

.
Now, in both cases of the or-formula, we can conclude merely
`max >= x ^ max >= y`

, as listed in the proof’s last line.

More precisely stated, the proof’s last line is
`(max >= x ^ max >= y) v (max >= x ^ max >= y)`

, but this is exactly the same
as `max >= x ^ max >= y`

.

We are not yet finished with this example; the desired goal is truly:

```
max >= x ^ max >= y ^ (max == x v max == y)
```

You should build a proof of this goal assertion by combining the two partial proofs that we have already constructed.

Here is the schematic of the forwards law for conditionals:

```
l"""{ ... P }"""
if (B) {
l"""{
1. B premise
2. P premise
...
}"""
C1
l"""{ ... Q1 }"""
} else {
l"""{
1. ~B premise
2. P premise
...
}"""
C2
l"""{ ... Q2 }"""
}
l"""{ 1. Q1 v Q2 premise }"""
```

That is, given the assertion, `P`

, at the conditional’s start, the then-arm,
`C1`

uses `P`

and `B`

to generate assertion, `Q1`

, and the else-arm,
`C2`

, uses `P`

and `~B`

to generate assertion `Q2`

.
These two conclusions are joined at the conditional’s conclusion.

When a conditional command lacks an else-arm, e.g.:

```
if (x < 0 ) {
x = 0 - x
}
```

we analyze it with an empty one, e.g., with an else-arm that holds pass:

```
var x: Z = readInt()
if (x < 0) {
l"""{ 1. x < 0 premise }"""
x = 0 - x
l"""{
1. x == 0 - x_old premise
2. x_old < 0 premise
3. x > 0 algebra 1 2
}"""
} else {
l"""{
1. ~(x < 0) premise
2. x >= 0 algebra 1
}"""
pass
l"""{ 1. x >= 0 premise }"""
}
l"""{
1. (x > 0) v (x >= 0) premise
2. {
3. x > 0 assume
4. x >= 0 algebra 3
}
5. {
6. x >= 0 assume
}
7. x >= 0 ore 1 2 5
}"""
```

Here, the conclusion of the if-command is `(x > 0) v (x >= 0)`

, but clearly
it is the case that `x > 0`

implies `x >= 0`

(and clearly, the other case,
`x >= 0`

implies ``x >= 0`

, holds), so we conclude at the very last line
that `x >= 0`

;
the justification is `ore`

— ``or elimination’’ — commonly known as
*proof by cases*.

Assertions that are disjunctions are cumbersome to handle, and we should avoid
them when possible.
Given that the forwards law for conditionals generates a disjunction, reflecting
the two possibilities for execution, it is important to learn how to reason
backwards from a goal through the arms of a conditional command.
As usual, we motivate the law through an example.
Using the previously seen program that assigns to `max`

, perhaps we want to
prove the goal, `max >= x ^ max >= y`

.
Our intuition tells us that this goal must be achieved through through both
paths of the conditional command.
That is, there are two subgoals to calculate, one for the then-arm and one for
the else-arm:

```
l"""{ subgoal_1 : ??? }"""
max = x
l"""{ goal: max >= x ^ max >= y }"""
```

and also

```
l"""{ subgoal_2 : ??? }"""
max = y
l"""{ goal: max >= x ^ max >= y }"""
```

Using the backwards assignment law, we calculate the subgoals for the two arms:

```
l"""{
subgoal_1: x >= x ^ x >= y
that is, x >= y (since x >= x is always true)
}"""
max = x
l"""{ goal: max >= x ^ max >= y }"""
```

and also:

```
l"""{
subgoal_2: y >= x ^ y >= y
that is, y >= x (since y >= y is always true)
}"""
max = y
l"""{ goal: max >= x ^ max >= y }"""
```

Now, given the extra knowledge that the conditional’s test is `x > y`

, we can
apply this knowledge to the subgoals.

First, the then-arm will achieve the final goal if the conditional’s test provides enough extra information to achive the subgoal:

```
x > y --> x >= y
```

The logical operator, `-->`

(read as “implies”), can be read as a
“logical if-then”: “if `x > y`

is assumed as a fact, then `x >= y`

follows
as a consequence”.
Or, read it as, “when `x > y`

holds true, then so must `x >= y`

”.

Similarly, the else-arm will achieve the final goal if the test provides enough extra information to achive the subgoal:

```
~(x > y) --> y >= x
```

Overall, the subgoal for the completed if-command is:

```
( x > y --> x >= y ) ^ ( ~(x > y) --> y >= x )
```

Here is a summary of what we have uncovered:

```
l"""{ if's subgoal: (x > y --> x >= y) ^ (~(x > y) --> y >= x) }"""
if (x > y) {
l"""{
subgoal_1: x >= x ^ x >= y
that is, x >= y
}"""
max = x
l"""{ goal: max >= x ^ max >= y }"""
} else {
l"""{
subgoal_2: y >= x ^ y >= y
that is, y >= x
}"""
max = y
l"""{ goal: max >= x ^ max >= y }"""
}
l"""{ final goal: max >= x ^ max >= y }"""
```

The implication operator, `-->`

, is new to us, and we must study it carefully,
which we do in a later chapter.
For now, pretend it is a “logical if”.

Let’s analyze the subgoal we calculated for the if-command.
First, is `x > y --> x >= y`

a true fact?
Well, whenever `x > y`

holds true, then by algebra, `x >= y`

must hold true,
too – the latter is a consequence of the assumption that `x > y`

holds true.
Similarly, `~(x > y) --> y >= x`

is a true fact, because whenever `~(x > y)`

holds, then `y >= x`

follows.
So, the subgoal is true, that is, `(x > y --> x >= y) ^ (~(x > y) --> y >= x)`

has the same meaning as `t`

. (and `v`

and `~`

and `^`

) - - -
literally, we must define an algebra for assertions, so that our logical
analysis is crystal clear.
We do this in a later chapter.

From the backwards proof, we can always rebuild the corresponding forwards proof. Here it is, for the example:

```
l"""{
assert: (x > y --> x >= y) ^ (~(x > y) --> y >= x)
This holds true.
}"""
if (x > y) {
l"""{
assert: the previous assertion ^ x > y
implies: x >= y
implies: x >= x ^ x >= y
}"""
max = x
l"""{ implies max >= x ^ max >= y }"""
} else {
l"""{
assert: the previous assertion ^ ~(x > y)
implies: y >= x
implies: y >= x ^ y >= y
}"""
max = y
l"""{ implies max >= x ^ max >= y }"""
}
l"""{
assert: (max >= x ^ max >= y) v (max >= x ^ max >= y)
implies: max >= x ^ max >= y
}"""
```

Here is an example where the desired goal is not always achieved:

```
var x: Z = readInt()
if (x > 0) {
x = 0 - x
} else {
pass
}
l"""{ goal: x >= 0 }"""
```

Using backwards reasoning, we quickly deduce that

```
var x: Z = readInt()
l"""{ if's subgoal: (x > 0 --> -x > 0) ^ (~(x > 0) --> x >= 0) }"""
if (x > 0) {
l"""{ subgoal: -x >= 0 }"""
x = 0 - x
l"""{ goal: x >= 0 }"""
} else {
l"""{ subgoal: x >= 0 }"""
pass
l"""{ goal: x >= 0 }"""
}
l"""{ goal: x >= 0 }"""
```

We see immediately there is *no way* that the if-subgoal holds true: clearly,
`(x > 0 --> -x > 0)`

is false, and `~(x > 0) --> x >= 0`

is false also
(for values of `x`

that are negative).
So, we cannot prove that the program achieves its goal.
Forwards reasoning also fails:

```
var x: Z = readInt()
if (x > 0) {
l"""{ x > 0 }"""
x = 0-x
l"""{
1. x = 0 - x_old premise
2. x_old > 0 premise
3. x < 0 algebra 1 2
}"""
} else {
l"""{
1. ~( x > 0) premise
2. x <= 0 algebra 1
}"""
pass
l"""{ 1. x <= 0 premise }"""
}
l"""{
assert: x < 0 v x <= 0
There is no way we can deduce x >= 0 ...
}"""
```

In contrast, say that we consider this variation of the example:

```
var x: Z = 0
if (x > 0) {
x = 0 - x
} else {
pass
}
l"""{ goal: x >= 0 }"""
```

We can prove, using either forwards or backwards reasoning, that this particular program achieves its goal (because we can deduce that the else-arm will be used). The precise reasoning will be presented in a later chapter.

We of course use conditional commands to avoid error situations. Consider

```
val x: Z = readInt()
val r: Z = readInt()
if (x != 0) {
r = 1.0 / x
} else {
r = 0
}
// print r
```

When the input number assigned to `x`

is nonzero, then the output, `r`

, will
be `x`

’s reciprocal.
The forwards reasoning that asserts this fact goes as follows:

```
val x: Z = readInt()
val r: Z = readInt()
if (x != 0) {
l"""{ ~(x == 0) }"""
r = 1.0 / x
l"""{ ~(x != 0) ^ r = 1.0/x }"""
} else {
l"""{ x == 0 }"""
r = 0
l"""{ x == 0 ^ r == 0 }"""
}
l"""{ (~(x == 0) ^ r = 1.0/x) v (x == 0 ^ r = 0) }"""
// print r
```

Once we learn better the deductive laws (the “algebra”) for `^`

, `v`

and
`-->`

, we can prove that:

```
(~(x == 0) ^ r == 1.0/x) v (x == 0 ^ r == 0)
```

says exactly the same thing as

```
(~(x == 0) --> r == 1.0/x) ^ ((x == 0) --> r == 0)
```

which reflects the strategy we had in mind when we wrote the conditional command.

Here are the two laws for reasoning about assignments:

First, recall that the notation, `[a/b]E`

, denotes phrase `E`

with all
occurrences of `b`

replaced by `a`

.
(Example: `[3 / x](2 * x * x)`

is `(2 * 3 * 3)`

.)

Here is the deduction law for an assignment command:

```
l"""{
...
m. P
}"""
x = e
l"""{
1. x == [x_old/x]e premise
2. [x_old/x]P premise
...
n. Q (where Q must _not_ mention x_old)
}"""
```

Given a goal, `G`

, we compute this subgoal:

```
l"""{ [e/x]G }"""
x = e
l"""{ G }"""
```

That is, the subgoal (precondition) required to achieve (postcondition) `G`

with the assignment is `[e/x]G`

.

```
l"""{ ... P }"""
if (B) {
l"""{
1. B premise
2. P premise
...
}"""
C1
l"""{ ... Q1 }"""
} else {
l"""{
1. ~B premise
2. P premise
...
}"""
C2
l"""{ ... Q2 }"""
}
l"""{ 1. Q1 v Q2 premise }"""
```

That is, if we deduce from precondition `B ^ P`

and commands `C1`

a
postcondition `Q1`

(and do the same for `C2`

, we can assemble the
postcondition `Q1 v Q2`

for the conditional.
(Of course, if `Q1`

is identical to `Q2`

, we can conclude just `Q1`

.)

```
l"""{ (B --> S1) ^ (~B --> S2) }"""
if (B) {
l"""{ S1 }"""
C1
l"""{ G }"""
} else {
l"""{ S2 }"""
C2
l"""{ G }"""
}
l"""{ G }"""
```

That is, if we deduce that `S1`

is the subgoal required by `C1`

to attain
goal `G`

(similarly for `C2`

), then the subgoal (precondition) needed to
attain the goal (postcondition) by the conditional is
`(B --> S1) ^ (~B --> S2)`

.

*
This note was adapted from David Schmidt's CIS 301, 2008,
Chapter 2
course note.
*