Read It Likea Computer

The frame of mind I try to achieve when tracking down elusive bugs (i.e. when all else has failed). Forget about what the code is 'supposed' to do and just blindly trace through what it tells me (acting as the computer) to do.

• FuturePerfectThinking
• UseTheSourceLuke.

---

So programmers need to be really good actors?

--- Given a good debugger - you don't have to. You can just sit through the show while the computer shows you step by step what it does

---

Actually, I'm going to disagree fairly violently with the concept presented here. A computer, or debugger, can only explore a finite swath of the state space described by your program. If you read it exactly like a computer, you are limiting yourself to the same finite exploration.

The most powerful thing you can do is analyze what the program does. In the case of loops, that means, first and foremost, knowing what the LoopInvariant? is.

Since a lot of the people I come across are not very familiar with this analysis tool, I'll present a trivial example. The goal is to compute the sum of the elements in an n-element array a[]. Sure, any of you can code this in your sleep. Here's the code:

 int sum = 0;
 int i

 for (i = 0; i != n; i++)
      sum += a[i];

See, I said it was going to be trivial! But have you ever thought about why this code works? How would you go about proving it, if you had to?

The first step is to write down the loop's invariant, which is:

 sum = summa{0 <= j < i} a[j]

I wish I had real mathematical notation here so I didn't have to fake it in Ascii. Oh well. It should be pretty easy to understand.

Now, the loop is correct whenever the following four conditions hold:

• The loop initialization establishes the invariant.

• If the invariant is true at the beginning of an iteration, it is also true at the end.

• On the loop termination, the invariant implies the correctness condition for the loop as a whole.

• Eventually, the loop will terminate.

Let's look at those in turn:

The loop initialization establishes the invariant

Here, the loop initialization is:

 sum = 0;
 i = 0;

Simply plugging those values into the invariant yields:

 0 = summa{0 <= j < 0} a[j]

This is true because it's an axiom of summation (one of the things you have to know if you're going to be in this business!).

If the invariant is true at the beginning of an iteration, it is also true at the end

This is the trickiest one. Let's use sum' and i' for the values of these variables at the end of the step. Then:

 sum' = sum + a[i]
 i' = i + 1

These equations are basically restatements in mathematics of the statements comprising the loop body. Let's also pull from our hat another axiom about summation (another one of those things you have to know):

 summa{0 <= j < i + 1) a[j] = a[i] + summa{0 <= j < i} a[j]

So, assuming the loop invariant holds for i and sum, does it hold for i' and sum'? Just plugging it in, the answer is yes. Cool.

[Incidentally, for real programs, this sum' notation is clunky. The Right Way to do this is with WeakestPreconditions?, but I didn't want to pull them into this example.]

On the loop termination, the invariant implies the correctness condition for the loop as a whole

The loop termination condition is:

 i = n

Plugging that in to the invariant yields:

 sum = summa{0 <= j < n} a[j]

...which tells us exactly what the loop computes!

Eventually, the loop will terminate

Ok, so this is another tricky one. The appropriate bit of mathematics is that the space of states forms a descending chain, with each loop iteration descending one level, and with the termination condition at the bottom. The simplest (and most often used) example of this is nonnegative integers: subtracting one each iteration, with zero at the bottom, does form a descending chain.

So, to establish it in this loop, the function I use is n - i. This function is zero when the termination condition is reached, and decreases by one every time I go around the loop. Thus, if it starts out as a nonnegative integer, I am guaranteed the loop will terminate. Working out the implications, this implies that the loop will terminate if n is nonnegative. Hmm, this is interesting, we've already found a way for this loop to hang, just start with n negative. What we have now is a precondition for correct execution.

So, I haven't read this program like a computer. I've analyzed it. I don't just have the intuition that it works, I know. Further, I also know the range of inputs for which it does work, and those for which it will fail. I think that's a win.

In addition, this technique gives me guidance about how to structure my loops. I always try to write them as follows:

 for (establish loop invariant, initialize termination function;
      !termination condition;
      go one step down in the decreasing chain for the termination function)
     reestablish invariant

Now, I admit that this level of analysis is probably too deep for most real programmers working on real programs. But I think that just knowing how to do it can give an intriguing fresh perspective on the problem you're trying to solve. Have fun!

-- RaphLevien