Как продемонстрировать корректность программы с циклом while, используя логику Хоара?

Как я могу продемонстрировать с помощью логики Хоара правильность программы, имеющей цикл while. Было бы интересно, если бы кто-нибудь развил его на любом примере, потому что моя проблема заключается в следующем:

Предварительное условие={n>0}

cont := n;
sum := 0;
while cont <> 0 do:
    sum := sum + cont;
    cont := cont-1;
endwhile

Постусловие={сумма=1+2+...+n}

Нет необходимости развивать этот пример. Мне просто нужно понять процедуру, потому что у меня нет практического примера. Спасибо за ваше время.


logic computation-theory hoare-logic proof proof-of-correctness
person Mandy007    schedule 12.02.2020    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Здесь должно применяться правило "while" логики Хоара:

Если команда S удовлетворяет тройке Хоара вида {P ∧ B} S {P}, то команда while B do S удовлетворяет {P} while B do S {P ∧ ¬B}.

Это единственный метод доказательства постусловия цикла while в логике Хоара, поэтому вы должны применить его. Условие B и тело цикла S задаются в коде, но P может быть любым условием, которое вы выберете, пока выполняется {P ∧ B} S {P}.

Эта тройка Хоара утверждает, что если P истинно до итерации цикла, то оно останется истинным и после, поэтому такое условие P известно как инвариант цикла. Чтобы доказать постусловие цикла, вам необходимо установить, (1) что P истинно до первой итерации цикла, и (2) что P сохраняется телом цикла.

Необходимый инвариант цикла в вашем примере — sum = n + (n-1) + ... + (cont+1), т.е. сумма чисел от cont+1 до n. В общем, не существует систематического способа найти правильный инвариант цикла; вы должны использовать свое понимание алгоритма и свою интуицию / опыт, чтобы придумать его самостоятельно.

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

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

person kaya3    schedule 14.02.2020