java - Java でのループ不変条件について

Question

私はループ不変条件を学んでおり、ますます難しい質問に挑戦してきました。今日、質問を解決しましたが、私の解決策が正しいかどうかわかりません。誰かが私の答えを確認して、解決策を与えるのではなく説明してもらえますか?

コード：

/**
 * @require a!= null && b!=null && a.size() == b.size() &&
 * !a.contains(null) && !b.contains(null)
 * @ensure \result is an array of size a.size() such that
 * for each index j of \result, c.get(j) is
 * the minimum of a.get(j) and b.get(j)
 */
public static List<Integer> pairwiseMin(List<Integer> a, List<Integer> b) {
    List<Integer> c = new ArrayList<Integer>();
    int i = 0;
    while (i < a.size()) {
        if (a.get(i) <= b.get(i)) {
            c.add(a.get(i));
        } else {
            c.add(b.get(i));
        }
        i++;
    }
    return c;
}

ループ不変条件:c.size() == i

質問：

c.size()==i述語がループ不変条件であるかどうかを簡単に説明してください。それがループ不変条件である場合、メソッドがその仕様に関して部分的に正しいことを検証するのに十分かどうかを説明してください. 述語がループ不変条件でない場合、またはメソッド pairwiseMin の部分的な正しさを検証するには不十分な場合は、メソッドが部分的に正しいことを示すために使用できるループ不変条件を定義します。

私の解決策：

はい、ループが実行される前後に前提条件事後条件が満たされるため、ループ不変です。

最初の反復:

expected: 
pre: i == 1;
post i == 2;

c.size() をチェック

pre: c.size() == 0;
post: c.size == 1;

したがって、部分的な正しさを証明するには十分です。