Recitation 9/17/97
- Questions on old quiz?
- Questions on assignment 2?
- Loop Invariants

(try and get through the first function.  If you have time do the second one as well)

What is this function doing?

(invariant: a*b + x = a0 * b0, where a0 and b0 are the initial values
of a and b)

    int f(int a, int b) {
	int x=0;
	while (b != 0) {

            // loop invariant goes here.

	    if (b&1 == 1) x += a;    // bitwise AND. I.e., is b odd?
	    b = (b >> 1);            // right shift: divide by two
	    a = (a << 1);            // left shift: multiply by two
	}
	return x;
    }

Micro level understanding of the code:

- The operator "&" is the bitwise and operator.  So "b&1" extracts the
  low order bit of b.  
- "b >> 1" shifts b to the right by 1, throwing away the low order
  bit.  For positive numbers, "b>>1" is the same as "b/2".
- Finally, "a<<1" means shift a to the left by 1.  This is exactly the
  same as "a*2".

Macro level understanding:

The way to understand what it does is to write a loop invariant that
relates the variables to eachother at the beginning of the loop.

Let a0 and b0 be the initial values of a and b.

The invariant is:  a*b + x = a0*b0

Proof of the invariant.

  (1) It holds the first time we enter the loop.
      This is obvious cause a=a0 and b=b0 and x=0;

  (2) The inductive step.  Let's let (a,b,x) be the values of the three
      variables at the beginning of an iteration of the loop.  Let a',
      b', x' be the values of those variables after that iteration of
      the loop.

      We know by induction that a*b + x = a0*b0.  There are two cases to
      verify depending on whether b is even or odd.  (In this analysis
      "/" is the ordinary mathematical definition of division.)

      b is even: Then b' = b/2, and a' = 2a and x' = x.
      so a'*b' + x' = a*2*b/2 + x = a*b + x.

      b is odd: Then b' = (b-1)/2, a' = 2*a, x' = x+a.
      a'*b'+x' = 2*a*(b-1)/2 + x+a = a*b-a + x+a = a*b + x.

      In both cases the quantity a*b + x remains constant, so the
      invariant holds.

Ok, now we just verified the invariant.  What does this function do?

At the beginning of the last iteration, we know that b=0.  The invariant
tells us that a*b+x = a0*b0.  But b=0, so we know that x = a0*b0.

Therefore at the start of the last iteration we know that x=a0*b0.  This
is the value returned by the function.  This completes the proof that
the function computes the product of a and b.

One thing missing: proof that it terminates.  All we've shown is that IF
it terminates, it computes the product of a and b.  Why does it
terminate?

It terminates because on each interation b is replaced by floor(b/2).
This is a decreasing function.  It must reach zero.  ask: How many iterations does it take?
It reaches zero in at most log2(b0) steps.

----------- If you have time.

EXAMPLE 2:

The following function takes as input a positive integer r.

    void g(int r) {
	int d = 0;
	int x = r;
	int y = 0;
	int dt;
	while (x >= y) {
	    plot the point (x, y);
	    d += 2*y + 1;
	    y++;
	    dt = d - 2*x+1;
	    if (dt > -d) {
		d = d - 2*x+1;
	        x--;
   	    }
        }
     }

What points does this function plot?

Before we can even begin to understand what this does, we need to figure
out the relationship between the variables during the loop.

Invariant: x^2 + y^2 - r^2 - d = 0.

Proof of the invariant:

  (1) It holds initially, because x=r, y=d=0 satisfies it.

  (2) Inductive step.  Assume it holds at the start of the loop.  By the
      time we reach the "if" statement, let d' be the new value of d,
      and y' be the new value of y.

      x'^2 + y'^2 - r^2 - d'  =  x^2 + (y+1)^2 - r^2 - (d+2y+1)  =

      x^2 + y^2 + 2y+1 - r^2 - d - (2y+1) = x^2 + y^2 -r^2 -d.

      So the invariant holds right before the "if" statement.

      If the "if" is false, nothing happens to the values of the
      variables.  If it is true, then x decreases by 1 
	(i.e., x'^2 = (x-1)^2 = x^2 -2x+1) 
      and d decreases by (2x-1).  An argument just like the above proves 
      that the invariant is maintained.


Termination.  The function terminates because on each iteration y
increases by 1 and x decreases by 0 or 1.  Eventually y must reach x.

What does the function actually do?

The invariant tells us that x^2+y^2-r^2 = d.  On each iteration, y
increases by 1 and x decreases by 1 or stays the same.  The criterion
used to decide what to do with x is to make the choice that keeps the
absolute value of d as small as possible.



                               |
                               |
                               |           0
                               |            0
                               |             0
                               |             0
                               |              0
                               |              0
                               |               0
                               |               0
              		       |	        0 
			       |	        0
			       | 	        0  
			       |	        0
        ----------------------------------------0------
			       |	       	
			       |	       	
			       |	       	
			       |	       	

So, this is in fact an algorithm for drawing a quarter of a circle.
Notice that it is implemented with no multiplications (multiplying by 2
is just shifting).