Инвариант цикла для функции для вычисления факториалов

Мне трудно правильно определить инвариант цикла для следующей функции:

F(y)
    X <-- 1
    while (y > 1)
        do x <-- x * y
           y <-- y - 1
    return (x)

Я определил инвариант цикла, чтобы быть x = 1 OR x = y! поскольку это утверждение верно как предварительное условие и верно как постусловие.

It doesn't seem to hold true for every iteration, as for example if y = 3, then on the first iteration of the loop, x = 1 * 3 which equates to 3 and NOT 3! which equates to 6.

Это то, где мое замешательство действительно, я думаю. В некоторых книгах говорится, что инвариант цикла - это оператор, который должен приравниваться к истине в начале или к циклу (таким образом, к предварительному условию), а также должен выполняться в конце цикла (таким образом, к постусловию), но не обязательно должен держите истинно часть пути через петлю.

Каков правильный инвариант цикла для функции выше?

Источник

2 ответа

Решение

Возможный инвариант цикла был бы x⋅y! = у 0! где y 0 - начальное значение y, которое передается в функцию. Это утверждение всегда верно, независимо от того, сколько итераций цикла уже сделано.

Предварительное условие должно сохраняться до начала цикла, постусловия должны сохраняться после завершения цикла, а инвариант должен удерживаться независимо от того, сколько итераций цикла было выполнено (поэтому он называется "инвариантным" - он не изменить это правда).

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

Источник

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

Вы знаете одну часть почтового условия: x == Y!, где Y это начальное значение, данное в качестве аргумента. y переменная, чье значение изменяется. И это остальная часть почтового условия, кстати: y == 1,

Что правда на каждом проходе? Причина в обратном направлении.

На последнем проходе x == Y*Y-1*...*2 and y == 2,

До этого? x == Y*Y-1*...*3 and y == 3,

До этого?

Что верно изначально, когда y == Y?

В заключение. Учитывая постусловие и инвариант, какое предварительное условие является самым слабым набором утверждений, необходимых для приведения вещей в движение? Код предполагает, x=1 and y=Y,

Вы знаете, что каждый раз, когда проходит цикл, что-то должно меняться, и программа должна продвигать состояние до постусловия. Это правда? Существует ли естественная функция состояния цикла, которая доказуемо уменьшается к нулю? (Это похоже на вопрос с подвохом, потому что y переменная, кажется, делает это тривиально. Это не очевидно во многих реальных циклах, поэтому вы должны задать вопрос о дизайне вашего цикла.)

Источник
Другие вопросы по тегам