Как я могу найти инвариант цикла и доказать правильность?

Question

Я учусь на правильность и изо всех сил пытаюсь найти соответствующий инвариант цикла и доказать его правильность.

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

SumPos(A[0..n - 1])
// Returns the sum of the positive numbers in an array A of length n. We
// assume that the sum of the numbers in an array of length zero is 
zero.
t = 0
i = 0
while i != n do
 if A[i] > 0
 t = t + A[i]
 i = i + 1
 return t

Answer 1

Прежде чем получить формальное выражение, иногда полезно подумать о том, «что остается прежним» и «что меняется» в отношении цикла . * Для написанного цикла у нас есть эти переменные, представляющие интерес:

• A - массив чисел для суммирования
• n - целое число элементов в A.
• t -как написано, я предполагаю, что предполагаемая сумма положительных сумм
• i - индексная переменная;иногда называют вариант

Так что меняет каждую итерацию?Массив A не меняется.Количество элементов n в массиве не изменяется.Как написано, сумма t может измениться.Переменная индекса i изменится .

Что касается цикла, то, как правило, люди говорят, что i является вариантом .Он увеличивает каждую итерацию, и его сравнение с n - это то, что выходит из цикла.

Инвариант, представляющий для меня интерес, заключается в том, что t всегда будет представлять вычисленную на данный момент сумму позитивов,Например, на первой итерации:

• До итерации i == 0 и t также правильно 0
• После итерации i == 1 и t будутбыть корректным по отношению к первому элементу.

Однако, как написано, оператор return исключает любую обработку за пределами первого элемента массива.Переходя от теории к практике, как тогда вы могли бы исправить реализацию?

* Для педантика важен классификатор, поскольку, строго говоря, «инвариант» - это то, что не меняется - не меняетсяили всегда выполняется - для каждой итерации цикла.Так? Множество операторов инвариантны относительно цикла!Например, имя моей матери инвариантно для цикла!