loops - ループ不変条件を使用したアルゴリズムの正確性

Question

ループ不変条件を使用して、以下のアルゴリズムの正確性を証明する必要があります。配列として表される 2 つの数値 (逆順: 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

このアルゴリズムに対してループ不変条件が何をすべきかがよくわかりません。前もって感謝します！