Нахождение инварианта цикла - Тройка Хоара

Question

Из следующего кода мне нужно вывести / выбрать инвариант цикла.

(|true|)
x = 0 ;
s = 0 ;
while ( x <= n ) {
    s = s + x ;
    x = x + 1 ;
}
(|s = n(n + 1)/2|)

Решение дано было

• s = (x-1)*x/2 ∧ (x ≤ n +1)

Я не совсем понимаю, как он достиг решения выше.

Пожалуйста, помогите мне с выводом такого решения или другого инварианта цикла из кода.

Answer 1

Учитывая инвариант, вы можете легко проверить, что он истинен до, внутри и после цикла (да, сложение целых чисел от 1 до n включительно дает вам (n+1)*n/2 - см. Треугольные числа). Поскольку он охватывает все соответствующие переменные в цикле (x а также s), и не может быть доработан (ну, вы можете добавить ^ x >= 0), это действительно инвариант.

Боюсь, что для того, чтобы сделать это самостоятельно, я боюсь, что вам нужно заранее знать формулу треугольных чисел (или половину квадрата). Можно конечно выписать что s = sum of integers from 1 to x для этой части, и я бы, например, принять его в качестве действительного инварианта. Часть где x <= n+1 сравнительно легко.

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

• s всегда содержит сумму целых чисел до х
• х проходит через целые числа от 0 до n включительно

А потом писать это по математике.