Понимание инвариантов цикла в 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; 
} 

Loop Инвариантная: c.size() == i

Вопрос:

Кратко объясните ли не предикат c.size()==i является инвариант цикла. Если это инвариант цикла, объясните, достаточно ли проверить, что метод частично корректен в отношении его спецификации. Если либо предикат не является инвариантом цикла, либо недостаточно проверить частичную корректность метода pairwiseMin, тогда определите инвариант цикла, который можно использовать, чтобы показать, что метод является частично правильным.

Мое решение:

Да, это инвариант цикла, так как предварительное условие пост условие выполняется до и после того, как цикл выполняется.

Первая итерация:

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

Проверить c.size()

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

Таким образом, достаточно доказать частичную правоту.

Answer 1

Я не совсем понимаю, о чем вы просите.

Но инвариант цикла не подходит.

Просто подумайте о том, что размер ArrayList b больше, чем a.

Это приведет к ошибке «Индекс за пределами границ».