Invariant For Nested Loop in Matrix Multiplication 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} &amp;= \sum_{k=1}^{n} A_{Ik}B_{kJ} &amp; \text{for all $I$ and $J$ such that $1\le I &lt; i$ and $1\le J\le n$}
  \\
\text{and}~~~ C_{iJ} &amp;= \sum_{k=1}^{n} A_{ik}B_{kJ} &amp; \text{for all $J$ such that $1\le J&lt; j$}
  \\
\text{and}~~~ C_{ij} &amp;= \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.