Invariant For Nested Loop in Matrix Program

[anggha.satya11]

Now I'm making a graduate thesis that will discuss 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:

Code: Select all

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? Is there 2 invariant in there or just one for that program?

Really thanks in advance.

[Goplat]

With a for loop, it's not clear whether the loop invariant should be defined as being true before the variable gets incremented, or after. So let's use more traditional Hoare-logic syntax and turn it into a while loop:

Code: Select all

k := 0;
while k ≠ n do
   k := k + 1;
   C(i,j) := A(i,k) * B(k,j) + C(i,j)
done


What we want to prove is that, given the precondition C(i,j) = 0, this code will establish the postcondition that C(i,j) equals the entry of the matrix product, i.e. C(i,j) = sum(k = 1 to n: A(i,k) * B(k,j)).

The Hoare rule for a while loop is:

Code: Select all

        {P ∧ B} S {P}
------------------------------
{P} while B do S done {¬B ∧ P}

The main thing the loop invariant P needs to do is describe the loop's progress in making our desired postcondition happen. At each iteration of the loop, C(i,j) is the sum of the first k products: C(i,j) = sum(x = 1 to k: A(i,x) * B(x,j)). Using that as the invariant would give us our postcondition; if C(i,j) is the sum of the first k products, and the loop condition B is now false (meaning k = n), then C(i,j) is the sum of all n products like we want.

Just one issue: the rule requires that we prove the loop body S actually preserves the invariant provided the condition is true initially ({P ∧ B} S {P}), and we can't quite do that yet because P is a nonsensical statement when k is out of bounds. So, we need to make the loop invariant express the fact that k will always be within bounds: the full loop invariant is 0 ≤ k ≤ n ∧ C(i,j) = sum(x = 1 to k: A(i,x) * B(x,j))

With this invariant, it should be possible to prove the inner loop does what it's supposed to. The other two loops will likewise have their own invariants describing their progress as they iterate (for the j loop: that the first j elements of row i of C are correct; for the i loop: that the first i rows of C are correct).

[anggha.satya11]

Really thanks for your answer sir. I have 2 questions about your aswer:

1. Can you explain more why you prefer while-loop than for-loop? i.e why the loop invariant will be not clear if we use for-loop?

2. OK, so my fault is previously I got the invariant is C(i,j) = sum(x = 1 to k: A(i,x) * B(x,j)), And you've explained why this is not "invariant" enough. But, if I can proof your invariant is truly invariant for innermost loop, how can I get the outer one? Must I consider the inner loop again or I can assume the inner loop is just a statement? Please advise.

Thank you very much sir.

[Goplat]

Can you explain more why you prefer while-loop than for-loop? i.e why the loop invariant will be not clear if we use for-loop?

The body of a for loop will not actually preserve a useful invariant by itself. The body combined with the (implied) increment of the loop variable does:

Code: Select all

-- C(i,j) is zero --
for k = 1 : n do
    -- C(i,j) is the sum of the first k-1 products --
    C(i,j) := A(i,k)*B(k,j) + C(i,j)
    -- C(i,j) is the sum of the first k products --
done
-- C(i,j) is the sum of all n products --

So proving correctness of a for loop is a little more confusing than a while loop because the so-called "invariant" is only true on one side of the body, and a slight modification of it (loop variable differing by one) is true on the other side. So it's probably easier to understand the while loop first. That's not to say that using for loops is necessarily a bad idea; in fact it will probably make the proof shorter overall for a program like this.

If we decide to base things on what's true at the end of the loop body (which I think for this particular program probably leads to fewer +1/-1s all over the place), then the following Hoare rule could be used:

Code: Select all

     {a≤i≤b ∧ P[i/i-1]} S {a≤i≤b ∧ P}
-------------------------------------------
{P[i/a-1]} for i = a : b do S done {P[i/b]}

If we define "for i = a : b do S done" to be equivalent to "i := a; while i ≤ b do S; i := i + 1 done", then this rule can be derived by using the invariant "a≤i≤b+1 ∧ P[i/i-1]" for the implied while loop.

2. OK, so my fault is previously I got the invariant is C(i,j) = sum(x = 1 to k: A(i,x) * B(x,j)), And you've explained why this is not "invariant" enough. But, if I can proof your invariant is truly invariant for innermost loop, how can I get the outer one? Must I consider the inner loop again or I can assume the inner loop is just a statement?

The outer loop does not need to be concerned with the implementation of the inner loop, only its precondition and postcondition.

What you may need to do is express that the inner loop doesn't affect things previously computed (rows before i, elements in row i before j), by adding appropriate clauses to its precondition and postcondition, and then to keep that correct those clauses will have to be added further up the derivation as well.

[anggha.satya11]

Thanks for your reply. Ok, from your first answer, I do agree that if I use the for-loop, the predicate (invariant) will not be explicitly "consistent" in the body of for-loop. So, this will be confusing. Am I right? By the way, I have successfully prove the inner loop program using Hoare logic with the invariant above. Thanks.

For my second question, I mean: I wanna proof the complete program. Not just the inner loop. Thus, I have to find the invariant for other loop, right? May I assume the inner loop is just a statement or how? For example for second loop:

Code: Select all

j = 0;
while (j~=n)
    j = j+1;
    k = 0;
    THIRDWHILE_STATEMENT
end


May I do like code above? Thus, I left to find the invariant for this second loop? But, how can I find the invariant? Must I still consider the

Code: Select all

THIRDWHILE_STATEMENT

or I don't need? Can you give me a clue sir?

Thank you very much.

[Goplat]

There's nothing special about nested loops; the inner loop is just another statement.