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    endendI'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?
Invariant For Nested Loop in Matrix Multiplication Program
algorithms;loop invariants;correctness proof