Invariant For Nested Loop in Matrix Multiplication Program

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?

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.

StackExchange Computer Science Q#1625, answer score: 11