3.3 Simple self referencing assignments

Now that we can handle constant assignments and a sequence, let's move on to something slightly more interesting.

Let us consider algorithm 2.

Note that the first two statements of algorithm 2 are the same as the first two statements of algorithm 1. Let's start with the first statement that is different. We know that $\rm {pre(\ref{selfassign1:xp3})} = (x = 0) \wedge (y = 2)$. What is the $\rm {post(\ref{selfassign1:xp3})}$?

Let us examine what we are doing on line 3. In this assignment statement, we first evaluate the right hand side. $x = 0$ at this point, so $x + 3 = 3$. Then, we take the value of 3, and use that to update $x$. In other words, $x = 3$ after the statement.

In the analysis of post conditions, we have a more obsure way to come to the same conclusion.

First, let us define a ``function'' $f(x) = x + 3$. This is really just a notation so that $f(3) = 6$, $f(-2) = 1$ and etc. When some functions, we can also define an ``inverse function''. In this case, the inverse function is $f^{-1}(x) = x - 3$. What this really means is simply that $f^{-1}(f(x)) = x$. In other words, $f^{-1}$ undoes whatever $f$ does.

Next, let us define a substitution operation. $\rm {sub(c,x,y)}$ means that in condition $c$, replace all occurances of $x$ with $y$. For example, $\rm {sub(x + y = z,y,y-1)} = x + (y-1) = z$.

With these new tools, we can get back to work. Let us keep the definition that $f(x) = x + 3$ and $f^{-1}(x) = x - 3$. Then we have the following derivation:

$$\rm {post(\ref{selfassign1:xp3})} = \rm {sub(\rm {pre(\ref{selfassign1:xp3})},x,f^{-1}(x))}$$ (7)

$$= \rm {sub((x = 0) \wedge (y = 2),x,x - 3)}$$ (8)

$$= ((x - 3) = 0) \wedge (y = 2)$$ (9)

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

Of course, this doesn't really come as a surprise. However, we now know why it is the case!

On to the last statement, we define $g(y) = y - 1$. The inverse function is $g^{-1}(y) = y + 1$ so that $g^{-1}(g(y)) = y$. Given this, we can finish the derivation:

$$\rm {post(\ref{selfassign1:ym1})} = \rm {sub(\rm {post(\ref{selfassign1:xp3})},y,g^{-1}(y))}$$ (11)

$$= \rm {sub((x = 3) \wedge (y = 2),y,y + 1)}$$ (12)

$$= (x = 3) \wedge ((y+1) = 2)$$ (13)

$$= (x = 3) \wedge (y = 1)$$ (14)

This is yet another earth-breaking discovery (not!). Although it may seem that we could have used intuition (sometimes called ``eyeball proof'') to come to the same conclusion, the tools that we have used in this section are very general and can be applied to much more difficult problems.

We can now derive the general case as follows:

Assume that $f(x)$ is a function of $x$ that has an inverse function $f^{-1}(x)$, then $\rm {post(1)} = \rm {sub(\rm {pre(1)},x,f^{-1}(x))}$.