1.  Add assertions and prove total correctness for the following
matrix multiplication program.


{  For every q,r  0<q<n, 0<r<n : res[q,r] = 0   }

i := 0;
while i ?  n loop

{           }

        j:=0;
	while j ? n loop

  {           }
                K:=0
		while k ? n loop
      
  	{           }
        	res[i,j] = res[i,j] + A[i,k] * B[k,j]
        	k := k + 1
        	{           }
 
        	end loop
        	j := j + 1
 	end loop
 	i := i + 1
 end loop
 
 {           }

---

Clarification of Question by haritha11-ga on 18 Mar 2005 09:45 PST

related matter is present in the text book "The Science of
Programming" by David Gries.