Loop инвариант и использование для решения алгоритма?

Question

Так что, если у меня есть следующий код:

public int sumSquares(int n){ 
    int sum = 0; 
    for(int i = 1; i <=n; i++){ 
     sum += i*i; 
    } 
    return sum; 
} 

теперь я должен найти инвариант цикла. Мне сказали, что для такой петли инвариант Y = i^2 считается инвариантом цикла, однако я не знаю, могу ли я доказать, что это инвариант цикла. Поскольку Y - это просто что-то, тогда оно всегда истинно до, во время и после цикла, потому что это то, что i * i ... Является ли это верным доказательством того, что он является инвариантом?

Также, когда дело доходит до доказательства алгоритма с инвариантом, правильно ли сказать, что sum = сумма от 1 до n i * i (или Y, инвариант цикла) = n (n + 1) (2n + 1)/6

Затем используйте индукцию, чтобы показать, что это правильно? Является ли это правильным использованием инварианта цикла для доказательства алгоритма?

Очень хотелось бы некоторую помощь :)

Answer 1

Инвариант должен быть, при входе в контур, для любого i,

sum = 0 + 1*1 + 2*2 + ... + (i-1)*(i-1) 

выше требование может быть доказано по индукции. Пусть sum будет переменная в начале цикла, а sum' переменную в его конце, то:

sum' = sum + i*i = 0 + 1*1 + ... + i*i 

Это позволяет использовать тот факт, что в addiiton, когда цикл завершается i=n+1, поэтому, когда программа заканчивается, вы получите:

sum = 0 + 1*1 + ... + n*n