Understanding Loop Invariants in Java

Question

I am learning loop invariants and I have been challenging myself with harder and harder questions. Today I solved a question, but I am unsure if my solution is correct. Can anyone please verify my answer, and please explain rather than just giving a solution?

Code:

/**
 * @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;
}

Loop Invariant: c.size() == i

Question:

Briefly explain whether or not the predicate c.size()==i is a loop invariant. If it is a loop invariant, explain whether or not it is sufficient to verify that method is partially correct with respect to its specification. If either the predicate isn’t a loop invariant, or it is not sufficient to verify the partial-correctness of method pairwiseMin, then define a loop invariant that can be used to show that the method is partially correct.

My Solution:

Yes it is a loop invariant because the precondition post condition is met before and after the loop is executed.

First iteration:

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

Check c.size()

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

Thus it is sufficient to prove partial correctness.

Answer 1

I am not clear about what you are asking.

But the loop invariant is not appropriate.

Just think about the case that the size of ArrayList b is larger than a.

It will cause to an error 'Index out of bounds'.