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

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

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.

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

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


function loops factorial invariants loop-invariant
person Brownbay    schedule 05.12.2011    source источник
comment
Инвариант цикла НЕ является постусловием. Все, что вы читали, что утверждало это, абсолютно неверно. Если вы нашли что-то, что подразумевало, что инвариант также был условием публикации, пожалуйста, включите ссылку или ссылку. Оно неполно или вводит в заблуждение. Инвариант, а НЕ условие while ЯВЛЯЕТСЯ постусловием.   -  person S.Lott    schedule 06.12.2011
comment
Я думаю, что я определенно неправильно прочитал утверждения автора. Я читал «Дискретную математику с приложениями» Сюзанны Эпп и предположил, что инвариант цикла представляет собой комбинацию условий до/после, когда кажется, что автор имел в виду, что инвариант цикла просто также гарантирует истинность условий до/после.   -  person Brownbay    schedule 06.12.2011
comment
автор имел в виду, что инвариант цикла просто также гарантирует истинность условий до/после. Учитывая это пересмотренное понимание, пожалуйста, обновите свой вопрос, чтобы попросить о помощи, которая вам действительно нужна.   -  person S.Lott    schedule 06.12.2011

Ответы (2)


arrow_upward
6
arrow_downward

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

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

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

person sth    schedule 05.12.2011
comment
Ваш инвариант цикла определенно имеет смысл и верен для нескольких примеров, которые я пробовал... Но ради аргумента, что было бы не так с альтернативным инвариантом цикла, например: x <= y! Просто он слишком расплывчатый? - person Brownbay; 06.12.2011
comment
@Brownbay: Проблемы обычно начинаются, когда вы пытаетесь использовать инвариант цикла, чтобы показать, что программа работает правильно. С помощью строгого инварианта цикла вы можете доказать, что функция действительно вернет правильный результат. Ваш инвариант цикла также полностью действителен, но, вероятно, слишком расплывчат, чтобы доказать правильность функции. Я предполагаю, что с инвариантом x <= y_0! вы можете только доказать, что алгоритм производит что-то меньшее или равное факториалу. - person sth; 06.12.2011

arrow_upward
1
arrow_downward

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

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

person S.Lott    schedule 06.12.2011