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

Я пытаюсь придумать инвариант цикла для следующего цикла 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) )