Hoare logi c * Здесь должно применяться правило"while":
Если команда S удовлетворяет тройке Хоара вида {P ∧ B} S {P} , тогда команда while B do S удовлетворяет {P} while B do S {P ∧ ¬B}.
Это единственная техника для доказательства постусловия while l oop в Hoare logi c, поэтому вы должны применить Это. Условие B и тело l oop S приведены в коде, но P может быть любым выбранным условием, если выполняется {P ∧ B} S {P}.
Эта тройка Хоара утверждает, что если P истинно до итерации l oop, то оно все равно будет истинно после, поэтому такое условие P известно как l oop инвариант . Чтобы доказать постусловие l oop, вам необходимо установить sh (1), что P истинно перед первой итерацией l oop, и (2) что P сохраняется в l oop body.
Необходимым инвариантом для l oop в вашем примере является sum = n + (n-1) + ... + (cont+1), т.е. сумма чисел от cont+1 до n. В общем, не существует систематического c способа найти правильный инвариант l oop для использования; Вы должны использовать свое понимание алгоритма и свою интуицию / опыт, чтобы придумать его самостоятельно.
Этого достаточно, чтобы показать, что , если l oop завершается тогда его постусловие будет выполнено; вам также нужно установить sh, что l oop действительно завершится. Техника, которую вы должны применить здесь, состоит в том, чтобы найти l oop вариант ; обычно это некоторая целочисленная величина, которая (1) уменьшается на каждой итерации l oop и (2) приводит к завершению l oop, когда количество достигает нуля.
В вашем примере cont является вариантом oop, поскольку l oop уменьшает cont := cont-1, а условие l oop завершает l oop, когда cont достигает нуля. В общем, как и при поиске полезного инварианта, не существует системной c процедуры, которая бы находила вариант во всех случаях, но вы можете начать с просмотра условия l oop, чтобы увидеть, какие переменные определяют, когда l oop заканчивается.