Teaching loop invariant choice

Question

This is in line with a prior question I asked about teaching induction, but this is specific to the loop invariant step.

I have not had great success helping my students see how to choose a loop invariant that will (1) always be correct (ie. actually be a loop invariant) and (2) create the structure that will allow them to actually prove that the algorithm in question will be able to behave correctly.

My personal mental process is simply to look at the final item you are trying to prove, and figure out what property of the loop will mimic that statement. While this seems to work well enough as an idiosyncratic process for me, it does not translate into a clear thought-process for the students who don't 'get it' naturally.

Does anyone have an idea about how to approach this with students to make it obvious?

Answer 1

Let's start with the term "Loop Invariance". It is a property of a loop that is true before and after each iteration, thus in-variant, non-changing. So then, what is the purpose of the loop invariance in proving algorithm correctness? That is, it is a predicate about what the loop is supposed to do. Thus with proof by induction on this predicate shows the correctness of this algorithm. I know this is still very theory heavy so let's break this down even more.

A simple insertion sort. The purpose of insertion sort is to sort an array. Therefore the loop invariance would be that after each i-th iteration, the array is sorted up to the i-th element. The magic here is that instead of looking at the nested for i, j, loops of the algorithm you are choosing the loop invariance that contributes to the goal of the algorithm.

To answer (1). There is no sure guarenteed way to choose the correct loop invariance unless you are very experienced in algorithm correctness through countless examples. The best approach is to choose the segment of code that is actually doing what the algorithm is trying to do. Such as the example above, sorted up to the i-th element.

(2). I believe this has to do with the proof itself, rather than understanding the loop invariance. Structurally, to prove that the algorithm is correct, you would have to use proof by induction (either simple, or complete) to pove the loop-invariance and the fact that the algorithm actually terminates. Usually proof of termination is a 1 liner, such as when i > array.length, loop will terminate.

simply to look at the final item you are trying to prove, and figure out what property of the loop will mimic that statement.

I can tell you are very intelligent as this is something only someone who truly understands algorithms and proof of correctness can say. It is actually very difficult for younger students to see this as they are tunnel-visioned by the actual loops in the code instead of the bigger picture. Instead, I think what you are trying to convey is to look for "what part of the code is doing what the algorithm is meant to do"

Answer 2

To give an explanation of this requires a problem in which to frame the discussion. I propose the Dutch National Flag problem, likely first proposed by Dijkstra, but I'm not positive.

I'll pose the problem first and discuss the solution using invariants.

The Problem Taken from The Science of Programming.

You have an array of n elements. Each element is a color, red, white, or blue. You want to "sort" the array so that all of the low index cells are red, all of the high index sells are blue, with the white cells between them.

The number of tests should be kept to a minimum. Cells may be permuted with swap (only). The algorithm you develop should require only a single pass over the array and be linear time.

---

This answer is in process and will be updated. If you want to try to solve it in the interim, the precondition is that the colors are randomly arranged and the postcondition is as described above: [red*, white*, blue*]

---

Discussion: There are many ways to develop a loop invariant, as discussed in Gries. One way is to weaken the postcondition. I will use [red*, white*, any*, blue*] as the weakened condition and the loop invariant. Such an array configuration can be described with three variables:

lastRed  
index  
firstBlue  

The definition of these is as follows: Every cell from 0 through lastRed is RED. Every cell from lastRed + 1 through index - 1 is WHITE. Every cell from lastBlue through the end is BLUE

To establish the invariant prior to the loop:

lastRed = -1;
index = 0;
firstBlue = flag.length; // flag is the array variable, initially random. 

With these definitions, the invariant is true with the array in state [ any* ].

Solution: The solution is to run a loop that takes the any* section from "all" to "empty". You can do that either by (a) increasing index, which breaks the invariant, and then re-establishing the invariant, or (b) by decreasing firstBlue and re-establishing. Looking at $flag[index]$ will tell you what to do. Swap two cells as needed. A three case "switch" or equivalent is the body of the loop.

The invariant along with index == firstBlue is the postcondition. Therefore the while loop test condition is index < firstBlue QED

Note that it is a linear pass over the array, but with two variables moving toward each other from the end. Cool as a moose.

---

Note 1: The Science of Programming book has many other ideas for coming up with an invariant. This was just one possibility. The book is well organized around that idea. In general, though, the invariant of a loop emerges somehow from the pre and/or postconditions.

Note 2: It shouldn't take much, after doing this exercise, to convince a student that with four values instead of three it is only a bit harder to "sort" in linear time. Actually, any list/array of values from a finite set can be sorted in linear time. Radix sort works, of course, but so does this.

Answer 3

Firstly, I believe that if the thought process is clear to you, then going through that process with your students, out loud, clearly and slowly, can help them understand what it is that you are trying to convey.

Go through that process for a number of various examples, which show how you decide on a loop invariant in the varying situations (yes, that pun was intended).

Whilst detailing every step in the thought process, you should elaborate on the things that are necessary for a loop invariant to be good. An example of what this means in the case of induction: There's the base case, and that should be relatively easy to understand. Then the hypothesis. From here the "oddities" begin. Go through the inductive step multiple times (it is a loop, after all ;)), and show them, explicitly, that the invariant really is invariant. A few inductive steps should make it clear how the invariant doesn't change.

From there it would depend on how many befuddled faces are looking at the board. If a relatively large portion of the class didn't grasp it, then repeat (note: this is kind of a loop invariant. You always check the same thing) the inductive steps' explanation. This is also useful to show how the algorithm behaves, because essentially you are debugging it¹, and so it shows how the invariant dictates the behavior.

I've seen the measure of student understanding of complex concepts being mostly Confused or Understood and there isn't much middle ground. When it looks like most students are less shocked then you can go through the last inductive step ($n-1$) and show how the loop invariant is still true, but it becomes false after going through the last step. This shows how the invariant choice no less than defines the algorithm's behavior.

---

¹Technically you're just executing the code line by line like a computer, but the point of what I said doesn't change.

Answer 4

At the CS1 level that I teach, I focus a lot on the role and the precise meaning of variables and encourage comments at the point of declaration that attempt to make these clear, especially variables that are involved in loops. Since the meaning of a variable changes as the loop body is executed, we "agree" to use the entry point as the standard point of reference.

This is admittedly not using the post-condition to derive the invariant which in turn would be used (in principle) to derive the code itself; but it helps students understand and check their code, and I hope lays the foundation for any exposure to semi-formal methods they might encounter in the future. Combining the termination condition with the assigned meanings of the variables allows me to make reference to the idea of program proofs. Admittedly, the bottom 2/3 of the class is rather lost there, but the top 1/3 is generally tantalized.

Answer 5

A great resource for the instructor to learn the max about invariants is to go to the master.

David Gries, The Science of Programming

It isn't a book for novice learners, though. But understanding what is in this book will help you a lot in teaching programming via invariants.

He reveals all. He and his son have an undergrad text book also, that might not be quite as deep as this.

In particular, David shows how to develop good invariants from postconditions.

Answer 6

Thinking of invariants shifts the focus of analysis from the how of detailed steps to the what in the essence of the problem. By lifting our eyes from the how, a unifying concept of the problem and its solution can emerge. As Dijkstra said, our brains are not really sufficient to the task of programming, and so we must find ways to ease the cognitive load, through techniques like "Separation of Concerns".

Looking at a problem abstractly, it is usually possible to set aside a lot of detail when first thinking about it. For example, I knew that a multi-threaded server would need some kind of Counting Semaphore to cap the number of simultaneous threads. I probably could have said something to that effect without knowing anything about programming. I assumed its characteristics, and later figured out how to construct one using a Mutex and Condition Variable.

It should be easy to find examples of everyday processes that are concisely described using invariants. A teeter-totter is constrained by the fact that the heights of the two sides have to sum to (roughly) a constant. A process that manages a buffer must ensure that the used plus unused amounts sum to the size of the array. Is it correct to say that in NP-type problems, we know the invariants / constraints, but not an algorithm?

If I come up with better examples, I will improve this answer. Qapla'!

Answer 7

Do it in code, so that pupils can play with it. This code will throw an exception if the invariant is not met. Show how this can be useful in finding bugs in the program.

The book a touch of class by Bertrand Meyer, is very good for teaching Object Oriented Programming and has examples (can't remember how many, but it is where I leant it).

loop_example is
   −− A loop example...
   local
      count: INTEGER
   do
      from
         count := 1
      invariant
         count >= 1
         count <= 101
      variant
         101 − count
      until
         count > 100
      loop
         io.put_integer (count)
         io.put_new_line
         count := count + 1
      end -- loop
  end -- method

The book has the philosophy that exceptions are only used for program bugs. variance, invariance, preconditions, and post conditions. Everything else should be checked traditionally. You will be surprised at how much simpler this makes things. You hardly ever see or use a catch clause. The philosophy makes it easy to get things right: if you forget to check an input, or have an out by one error, then the program will tell you that you have a bug, and tell you where it is.