Understanding loop invariants in Java Baeldung

I am studying loop invariants and I have challenged myself. Today I solved the question, but I'm not sure if the solution is correct. Can anyone please validate my answer and explain rather than just give 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;
}

      

        
        
        
      

    

Cycle invariant: c.size() == i

Question:

Briefly explain whether the predicate is a c.size()==i

loop invariant. If it is a loop invariant, explain if it is enough to check that the method is partially correct in terms of its specification. If either the predicate is not a loop invariant, or it is not enough to test the partial correctness of the pairwiseMin method, then define a loop invariant that can be used to show that the method is partially correct.

My decision:

Yes, it is a loop invariant because the postcondition 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 enough to prove the partial correctness.