loops - 使用循环不变量的算法正确性

Question

我必须使用循环不变量来证明下面算法的正确性。它需要两个表示为数组的数字（倒序：1579 -> [9 7 5 1]），处理它们的乘法并将结果作为数组返回。

ArraysMultiplication(x,y,n)
In: x, y — the numbers represented as arrays
In: n — the length of arrays
Out:  p (the array that contains the multiplication result)
for i = 0; 2n - 1 do
    p[i] = 0
end for
for i = 0; n - 1 do
    remainder = 0
    for j = 0; n - 1 do
        value = x[j] * y[i] + remainder + p[j + i]
        p[j + i] = value mod 10
        remainder = value div 10
    end for
    p[n + i] = remainder
end for
return p

我真的不明白循环不变量应该为这个算法做什么。提前致谢！