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

Question

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

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

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

Кажется, что это не выполняется для каждой итерации, например, если y = 3, то на первой итерации цикла x = 1 * 3, что равно 3, а НЕ 3! что равно 6.

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

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

Answer 1

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

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

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

Answer 2

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

Вам известна одна часть условия записи: 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, кажется, делает это тривиально. Во многих реальных циклах это неочевидно, поэтому вам нужно задать вопрос о дизайне вашего цикла.)