Как найти самый сильный инвариант цикла для этого кода?

Question

Я пытаюсь придумать инвариант цикла для следующего цикла while, но у меня возникли некоторые проблемы.

После того, как инвариант цикла определен, я хотел бы собрать таблицу доказательства ипоказать все промежуточные утверждения

ASSERT(k >= 0)
{i = 1;
 sum = 1;
 while (i <= k) { 
     sum = sum + 2*i + 1;
     i = i+1;
 } //end-while
}
ASSERT( sum == (k+1)*(k+1) )

Answer 1

INV(1) = {sum == (n+1)*(n+1)}  
INV(2) = {0<=n<=k}

сумма = 1 работает для n = 0
Теперь попробуйте доказать, что он работает для n + 1 (если верно для n), пока n не достигнет k (в вашем случае, мой n будет вашим i)

Answer 2

Обратите внимание, что когда он существует в цикле, значение i равно k+1, то есть хороший инвариант выглядит так:

INV(1) = {1 <= i <= k+1}

INV(2) = {sum == i*i}