7
$\begingroup$

I'm making a graduate thesis about proving correctness of program for multiplying 2 matrices using Hoare logic. For doing this, I need to generate the invariant for nested loop for this program:

for i = 1:n
    for j = 1:n
        for k = 1:n
            C(i,j) = A(i,k)*B(k,j) + C(i,j);
        end
    end
end

I've tried to find the invariant for inner loop first, but I can't find the true one until now. Is there someone can help me for finding the invariant for above program?

$\endgroup$

migrated from cstheory.stackexchange.com May 2 '12 at 2:57

This question came from our site for theoretical computer scientists and researchers in related fields.

11
$\begingroup$

You need the line C(i:j) = 0 just before the innermost loop; otherwise, the code is incorrect.

Assuming that line is in place, here is the (strongest possible) invariant just before the assignment in the innermost loop: \begin{align*} C_{IJ} &= \sum_{k=1}^{n} A_{Ik}B_{kJ} & \text{for all $I$ and $J$ such that $1\le I < i$ and $1\le J\le n$} \\ \text{and}~~~ C_{iJ} &= \sum_{k=1}^{n} A_{ik}B_{kJ} & \text{for all $J$ such that $1\le J< j$} \\ \text{and}~~~ C_{ij} &= \sum_{K=1}^{k-1} A_{iK}B_{Kj}. \end{align*} (Yes, the whole thing.) The invariant just after the assignment has $k$ in place of $k-1$ in the last sum, but is otherwise identical.

$\endgroup$
  • $\begingroup$ Prof, I sent you an email. Sorry if I disturb you. :) $\endgroup$ – asn32 May 2 '12 at 19:56
2
$\begingroup$

There is no such thing as “the” invariant: any loop has plenty of invariants. You need to find an interesting invariant. Since you're trying to prove that the loop computes a matrix multiplication, your invariant must imply that when $i=j=k=n$, the coefficients of $C$ are those of the matrix product $A \times B$, i.e. $$\forall i \in [1,n], \forall j \in [1,n], C(i,j) = \sum_{k=1}^n A(i,k) \cdot B(k,j)$$ It is rather natural to specialize this property of $i$ and $j$ to conjecture an invariant for the outer and middle loops:

  • $\forall j \in [1,n], C(i,j) = \sum_{k=1}^n A(i,k) \cdot B(k,j)$ on the outer loop
  • $C(i,j) = \sum_{k=1}^n A(i,k) \cdot B(k,j)$ on the middle loop

Each run of the inner loop adds the $k$th term to the sum, which leads to the proposed invariant: $$C(i,j) = \sum_{l=1}^k A(i,l) \cdot B(l,j)$$ It's easy to see that if this invariant holds, then the proposed invariant for the middle loop holds, and from that, the proposed invariant for the outer loop holds, and the program does what is expected.

What remains to be proved is the initial condition. You need to prove that $\forall i, \forall j, C(i,j) = \sum_{l=1}^0 A(i,l) \cdot B(l,j)$, i.e. $\forall i, \forall j, C(i,j) = 0$ on entry to the program. You had better initialize $C$ so that this is so. Alternatively, you can achieve this property by doing the initialization inside the middle loop, just before entering the inner loop.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.