3.1 Constant assignment

Let's start with something that's relatively simple to deal with. Algorithm 1 is just a sequence of assignment statements.

Assuming this algorithm stands alone, there is no pre condition to it. In our notation, $\rm {pre(1)}$ represents the pre condition of the statement on line 1. Because line 1 is the first line of code, $\rm {pre(1)}$ also represents the pre condition of the entire algorithm.

Note that a pre condition is a condition. It expresses something that is true. How do we express true when we don't know anything is true? Well, we know something is always true, it is ``true'' itself!

Consequently, we can simply say that $\rm {pre(1)} = \rm {true}$.

What is the post condition of line 1? Since this is a constant assignment statement, we know that variable $x$ must end up with a value of 0. In other words, we know that $x = 0$ after this statement. Consequently, we ``add'' the fact to $\rm {pre(1)}$ so that $\rm {post(\ref{constassign1:x0})} = \rm {pre(\ref{constassign1:x0})} \wedge (x = 0)$ If you look up the definition of conjunction, $x \wedge true$ is simply $x$. We can simplify our post condition so that $\rm {post(\ref{constassign1:x0})} = (x = 0)$.

The same argument applies to line 2. Note that $\rm {pre(\ref{constassign1:y2})} = \rm {post(\ref{constassign1:x0})}$ because there is nothing that can change what we know about the program between the lines. What is $\rm {post(\ref{constassign1:y2})}$?

Line 2 changes variable $y$ to a constant of $2$. We know that after line 2, $y = 2$. However, this is not the only thing that we know. What we knew earlier that $x = 0$ is still true. As a result, $\rm {post(\ref{constassign1:y2})} = (x = 0) \wedge (y = 2)$.

Here comes the tricky part. What is $\rm {post(\ref{constassign1:x5})}$? If we simply add the fact that $x = 5$, then we end up with $\rm {post(\ref{constassign1:x5})} = (x = 0) \wedge (y = 2) \wedge (x = 5)$. However, this is impossible because $x = 0$ contradicts $x = 5$. What do we need to do?

What we need is a way to ``forget'' some facts because a new fact is in, and the new fact may contradicts some old facts. This is accomplished by a ``forget'' operation. let us define $\rm {forget(c,v)}$ to mean forgetting all components in condition $c$ that refers to variable $v$.

In our example, we can now derive $\rm {post(\ref{constassign1:x5})} = \rm {forget(\rm {post(\ref{constassign1:y2})},x)} \wedge (x = 5)$. Literally, this means ``the post condition of line 3 is essentially the same as the post condition of line 2, except that all components referring to $x$ should be forgotten. Then, we add the fact that $x = 5$.''

This results in the following derivation:

$$\rm {post(\ref{constassign1:x5})} = \rm {forget(\rm {post(\ref{constassign1:y2})},x)} \wedge (x = 5)$$ (1)

$$= \rm {forget((x = 0) \wedge (y = 2),x)} \wedge (x = 5)$$ (2)

$$= (y = 2) \wedge (x = 5)$$ (3)

Now, onto the last statement. We only have to reapply what we learned in the previous step:

$$\rm {post(\ref{constassign1:y1})} = \rm {forget(\rm {post(\ref{constassign1:x5})},y)} \wedge (y = 1)$$ (4)

$$= \rm {forget((y = 2) \wedge (x = 5),y)} \wedge (y = 1)$$ (5)

$$= (x = 5) \wedge (y = 1)$$ (6)

Are you surprised at the result?

Let us consider the general case:

Assuming $e$ does not refer to variable $x$ itself, then $\rm {post(1)} = \rm {forget(\rm {pre(1)},x)} \wedge (x = e)$.