Solutions to quiz 2
-------------------

Make sure you understand these solutions.  The idea was to give the
important postconditions and loop invariants, not just what range the
loop counters go over.  Specifications are supposed to tell you
PRECISELY what the code accomplishes.

Try to prove these specifications are correct.
  - prove the loop invariants are true (using induction)
  - prove partial correctness:
       i.e., assuming the loop invariant is true, and assuming the
       loop terminates, prove that the postcondition is true.
     (This should be easy).
  - prove the loops terminate (fairly obvious here)

----------------------

OUTER LOOP

Postcondition

  - ut is true if the matrix M is upper triangular, and false otherwise
 
  OR (more mathematically)

  - ut is true if M(i,j) = 0 for all i,j such that
         j < i <= n  and 1 <= j <= n


Precondition

  - M is an nXn matrix of integers
  - col = 1
  - ut is true

Loop Invariant  (NOTE HOW THESE ARE SIMILAR TO THE POSTCONDITIONS)

  - ut is true if there are zeroes below the main diagonal for
    columns 1 .. col-1 of M, and false otherwise

  OR (more mathematically)

  - ut is true if M(i,j) is zero for all i,j such that 
          j < i <= n and 1 <= j <= (col-1)


INNER LOOP

Are these loop invariants?

a.  NO  because at the last iteration, before exit, row = n+1

b.  YES because row starts out as col+1 and always gets bigger

c.  NO  because ut might be false when there is a zero in position
        M(row,col).  This would happen with a matrix like:

		1 1 1 1
                0 1 1 1  when col=1, and row=4, ut would be false, 
                1 0 1 1       but M(row,col) = 0
                0 0 0 1

d.  NO  because this is not true at the first iteration.  It says that
        at the start of the very first iteration, the value at
        M(row,col) is zero if ut is true, but we haven't even checked
        that value yet.  At the start of the first iteraion, we
        haven't checked any of the column yet.  The next invariant
        fixes that.

e.  YES because this is always true at the beginning of every iteration.
        At the start of the first iteration row=col+1, so the range
	col+1..row-1  is  col+1..col which means an empty range.