Teaching Programming to Liberal Arts Students:Using Loop Invariants

Prologue

Introduction

The Context

Introducing Loop Invariants

• give a preliminary definition of a loop invariant: it is an assertion that is true just before the while statement and just after the loop body and
• point out that by its very nature, a loop invariant will also be true immediately after the while statement.

x := 0;						n := m;
while x<20 do begin		t := 0;
  	x := x+5				while t<10 do begin
end							    t := t+1;
							        n := n+1
						       end

Consider the following loop:

	x := 0;
	while x<>a do begin
		... loop body ...
	end

Given that a>b is a loop invariant what assertions will be true after the while statement? What can be said about the relationship between x and b after the loop?

Using Loop Invariants

1. Determine the variables needed for the loop.
2. Express the condition that is desired after the loop (the goal of the loop).
3. Extract from this condition the loop invariant and the while condition.
4. Use the information from (3) to write the loop.

1. We will write code to divide by repeated subtraction. The count of how many subtractions we do will be the quotient and whatever is left when we can't subtract any more (i.e. when the result of subtraction would be negative)- that will be our remainder.
2. (We need a variable to hold our dividend, a variable to hold our divisor, a variable to hold what is left so far (the remainder) and a variable to hold the count of how many times we have subtracted (the quotient). Let's call them a,b,r,q respectively.
3. When we have finished looping a=q*b+r and guaranteeing that we've gone sufficiently but not too far, 0<=r<y.
4. Let's pick the loop termination condition as r<y and voilà: the loop condition is r>=b and the invariant is a=q*b+r and r>=0.

(1) Work out in detail a numerical example of dividing by repeated subtraction. Better yet, illustrate it graphically. Let's try, for example, 13/4. We start with, say, 13 triangles, and proceed to discover how many groups of 4 we can make. While doing so, we keep track of all relevant values in each step.

(2a) Where's the invariant? At this point it is easy for the students to recognize what is invariant here. Even the weakest can see that the total number of triangles is constant and nearly all can see that at each step of the way the total equals the number of groups times the groupsize plus whatever is left.
(2b) When do you stop? Similarly, virtually all the students can articulate the termination condition: the procedure must stop when the number left is less than the groupsize.
(2c) How do you ever stop? Again, virtually all the students realize that the algorithm advances towards termination by making a new group (doing a subtraction) at each step.
(3) Choose variable names for each quantity referred to in the procedure above:

	var	a:	integer,	{ number of triangles	}
		b:	integer,	{ group size		}
		q:	integer;	{ number of groups	}
		r:	integer;	{ what's left		}

(4) Once variable names have been chosen, the student can express steps (2a-2c) as assertions and code fragments:

(4a) Invariant: a=q*b + r
(4b) When to stop: r<y
(4c) Make progress to termination: q := q+1

(5) The student can the put the pieces of (4a-4c) together:

		{Invariant: a=q*b + r}
		while r>=y do begin
			r := r - b
			q := q+1
		end

(6) Finally the student must make sure that the invariant is satisfied, before the loop and then at the end of each loop body. Since there are many ways of initially satisfying a=q*b+r for a given a,b, the student, like any sensible person, will allow herself to be guided by the informal strategy worked out above and use the invariant as a check (q:=0;r:=a). The same is not true for the loop body: if a=q*b+r is true before the loop body and q is incremented by 1 then only decrementing r by b will restore the balance. Most students though will not take this calculational approach but still let themselves be guided here by the informal strategy and use the invariant as a check.

• the students discover for themselves a useful invariant (if not the full invariant) and the termination condition before writing any code;
• they use this information to guide them in their coding.

Conclusion

• Loop invariants should be introduced simultaneously with the while statement itself and used initially as a means for analysing loops.
• Students will find loop invariants more accessible and hence helpful if they learn to derive them from a consideration of the loop strategy rather than from the condition that is desired at the end of the loop.

References