Contents

1 About this module

• Prerequisites: 0011, 0012, 0013
• Objectives: This module introduces the concepts of pre and post conditions for various types of statements.

2 What is this crazy math?

So you thought it’d be easy becoming a programmer.

There are two schools of thought regarding the role of mathematics in programming. One school, led by Edsger Dijkstra, suggests that a programmer should be mathematician first. At the very least, every programmer should have a solid foundation of mathematics. Furthermore, computer science should be a branch of mathematics. For a more detailed discussion of this topic, visit http://en.wikipedia.org, and search for “cruelty computer science”.

Another school, including Donald Knuth (another giant and pioneer of computer science), claims that with sufficient advances of tools, everyone can program computers. This is at least partially true. In the “good old days”, programs are only written in machine language, consisting of long strings of 0’s and 1’s. Later on, with symbolic assemblers, writing programs became easier. These days, with Visual Studio and other development environments, the tools actually helps to fix problems not only in syntax, but also sometimes the logic of programs.

Nonetheless, it is still important for programmers to understand enough logic and mathematics. Programming by intuition is possible, but it only enables a programmer to a certain level. If not for anything else, a solid background of logic and mathematics enables a programmer trouble shoot faulty programs with great efficiency. Most programmers who are well trained in mathematics also tend to design more elegant programs that minimize chances of errors to begin with.

3 Pre and post conditions

A pre condition is simply “what we know before the execution of a statement in a program.” A post condition is “what we know after the execution of a statement in a program.” The analysis of the pre and post conditions of a program is essential, because we can prove the correctness of a program (or an algorithm) rigorously.

If you consider an algorithm, the pre condition of the entire algorithm is what is given to the program. The post condition of an entire algorithm is the outcome of a program. Being able to mathematically derive the post condition of an algorithm based on its pre condition means we can prove whether an algorithm does what it is supposed to. There is no need to use test cases anymore, because a proof of correctness covers all cases that can be thrown at the algorithm.

3.1 Constant assignment

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

Assuming this algorithm stands alone, there is no pre condition to it. In our notation, $pre\left(1\right)$ represents the pre condition of the statement on line 1. Because line 1 is the first line of code, $pre\left(1\right)$ 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 $pre\left(1\right)=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 $pre\left(1\right)$ so that $post\left(1\right)=pre\left(1\right)\wedge \left(x=0\right)$ If you look up the definition of conjunction, $x\wedge true$ is simply $x$. We can simplify our post condition so that $post\left(1\right)=\left(x=0\right)$.

The same argument applies to line 2. Note that $pre\left(2\right)=post\left(1\right)$ because there is nothing that can change what we know about the program between the lines. What is $post\left(2\right)$?

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, $post\left(2\right)=\left(x=0\right)\wedge \left(y=2\right)$.

Here comes the tricky part. What is $post\left(3\right)$? If we simply add the fact that $x=5$, then we end up with $post\left(3\right)=\left(x=0\right)\wedge \left(y=2\right)\wedge \left(x=5\right)$. 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 $forget\left(c,v\right)$ to mean forgetting all components in condition $c$ that refers to variable $v$.

In our example, we can now derive $post\left(3\right)=forget\left(post\left(2\right),x\right)\wedge \left(x=5\right)$. 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:

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

Are you surprised at the result?

Let us consider the general case:

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

3.2 Resolving references to variables to constants

If there are any “chainable” equalities, you should try to get everything resolved to constants whenever possible. For example, let us consider the following post condition:

$post\left(1\right)=\left(x<y\right)\wedge \left(y=10\right)$

Here, we already know, for sure, that $y$ has a value of 10. This means that the inequality $\left(x<y\right)$ can now be resolved as $\left(x<10\right)$. The main purpose to do this is to decouple variables from each other. In other words, we want to lessen the impact of a change to one variable to conditions that involve other variables.

In this example, a later assignment can change the value of $y$. However, that will not impact the fact that we already know that $\left(x<10\right)$.

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

Note that the first two statements of algorithm 3.3 are the same as the first two statements of algorithm 3.1. Let’s start with the first statement that is different. We know that $pre\left(3\right)=\left(x=0\right)\wedge \left(y=2\right)$. What is the $post\left(3\right)$?

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\left(x\right)=x+3$. This is really just a notation so that $f\left(3\right)=6$, $f\left(-2\right)=1$ and etc. When some functions, we can also define an “inverse function”. In this case, the inverse function is $f^{-1}\left(x\right)=x-3$. What this really means is simply that $f^{-1}\left(f\left(x\right)\right)=x$. In other words, $f^{-1}$ undoes whatever $f$ does.

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

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

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\left(y\right)=y-1$. The inverse function is $g^{-1}\left(y\right)=y+1$ so that $g^{-1}\left(g\left(y\right)\right)=y$. Given this, we can finish the derivation:

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\left(x\right)$ is a function of $x$ that has an inverse function $f^{-1}\left(x\right)$, then $post\left(1\right)=sub\left(pre\left(1\right),x,f^{-1}\left(x\right)\right)$.

3.4 Revisiting the Forget operation

The forget operation is applicable for assignment statements whenever the substitution operation cannot be performed. This means that the following statement should use the “forget” operation:

This is because the RHS of the assignment does not refer to the LHS. There is no inverse function to reverse the new value of $x$ back to its previous value before the assignment statement.

As a result, you can use the substitution rule if and only if the following conditions are all true for an assignment statement $x\leftarrow e$ ($e$ is an expression):

• The RHS ($e$) refers to the LHS. If so, let us define $f\left(x\right)=e$
• There is an inverse function $f^{\prime }\left(x\right)$ such that $f^{\prime }\left(f\left(x\right)\right)=x$

For all other assignment statements, the forget rule should be used. This include the following statement:

This is because even though the RHS refers to the LHS in this case, it is not reversible. Once variable $x$ becomes zero after this statement, there is no way to “recover” its previous value before the assignment statement.

3.5 Conditional statements

Let’s consider algorithm 3.5 that makes $z$ the maximum of $x$ and $y$.

Let us express the pre and post conditions of each statement. In this case, let us not to assume any values in the variables. In other words, $pre\left(1\right)=true$

The pre condition of line 2 is not just $true$. This is because the only way that we get to line 2 is that the condition $x>y$ must be true. Consequently, $pre\left(2\right)=\left(x>y\right)$. Using the same argument, the only way we get to line 4 is that $\neg \left(x>y\right)$, which is equivalent to saying $x\le y$. As a result, $pre\left(4\right)=\left(x\le y\right)$.

The post condition of line 2 is simply $post\left(2\right)=pre\left(2\right)\wedge \left(z=x\right)=\left(x>y\right)\wedge \left(z=x\right)$. Similarly, the post condition of line 4 is $post\left(4\right)=pre\left(4\right)\wedge \left(z=y\right)=\left(x\le y\right)\wedge \left(z=y\right)$.

Here comes the tricky part: what is $post\left(5\right)$? In other words, after the entire conditional statement, what can we conclude?

There are two ways to get to line 5. We can get there from line 2, or from line 4. Consequently, the post condition of line 5 is the post condition of line 2 or the post condition of line 4. In other words,

Does this make sense?

Here is the general conditional statement:

• $pre\left(2\right)=pre\left(1\right)\wedge c$
• $pre\left(4\right)=pre\left(1\right)\wedge \neg c$
• $post\left(2\right)$ has no general form, it depends on the actual code of “then-block”. Note that even $c$ may not true after the code of “then-block”.
• $post\left(4\right)$ has no general form, it depends on the actual code of “else-block”. Note that $c$ may actually be true after the code of “else-block”.
• $post\left(5\right)=post\left(2\right)\vee post\left(4\right)$

3.6 Loops

We are now on our final stretch!

Let us consider algorithm 3.6.

Let’s begin with $pre\left(2\right)$. After the initialization of $x$, we know that $pre\left(2\right)=\left(x=0\right)$. However, the post condition of line 2 is not as simple. This is because there are actually two ways to get to line 2. In the first iteration, we enter from line 1. However, in subsequent iterations, we enter from line 3. On the other hand, no matter which way we come from, we know that the condition $\left(x<3\right)$ must be true if we enter the loop.

As a result, all we say at this time is that $post\left(2\right)=\left(x<3\right)\wedge \left(\left(x=0\right)\vee post\left(3\right)\right)$. Note that $pre\left(3\right)=post\left(2\right)$.

The statement on line 3 looks familiar. It involves a function of $x$. In this case, the inverse function is $x-1$. We can then derive the following:

This is interesting because the same notation appears on the left and the right hand side of the equation. The solution is to find a definition that works in this equation. Choosing $post\left(3\right)=\left(x\le 3\right)$ works. This is because $\left(x=1\right)\vee \left(x\le 3\right)$ simplifies to $x\le 3$ because it includes the case of $x=1$. Furthermore, $\left(x\le 3\right)\wedge \left(x\le 3\right)$ can also simplify to just $x\le 3$. In conclusion, we can define $post\left(3\right)=\left(x\le 3\right)$.

How about $post\left(4\right)$? In theory, we can get there using two means. First, it is possible not to enter the loop at all. Second, we can go through the loop at least once, then exit the loop. Regardless of whether we get into the loop or not, one thing is for sure: $x<3$ must be false. As a result,

In other words, when we exit the loop, we know that $x=3$.

In its general form, a prechecking loop is as follows:

• $post\left(1\right)=pre\left(2\right)=c\wedge \left(pre\left(1\right)\vee post\left(2\right)\right)$
• $post\left(3\right)=\neg c\wedge \left(pre\left(1\right)\vee post\left(2\right)\right)$
• The trick is to find a good definition of $post\left(2\right)$! $post\left(2\right)$ is also called the “loop invariant”.

The general form of a postchecking loop is as follows:

• $pre\left(2\right)=pre\left(1\right)\vee post\left(2\right)$
• $post\left(3\right)=c\wedge post\left(2\right)$
• Again, the trick is to find a good definition for $post\left(2\right)$, it is also called the “loop invariant”.