Для целей доказательства правильности программ к правилам исчисления предикатов следует добавить правила, необходимые для выполнения последовательности операторов программы. Эти правила, называемые правилами следствия, формулируются следующим образом:
1) если {P}S{Q} и Q Þ R, то {P}S{R};
2) если {Q}S{R} и P Þ Q, то {P}S{R}.
Первое правило заключается в следующем: «Если P — предусловие для Q и если Q Þ R является теоремой исчисления предикатов, то P — предусловие для R». Таким образом, если P истинно и выполняется S, то R (так же, как и Q) истинно.
Второе правило следствия аналогично данному. Эти правила следствия можно представить в более формальном виде: числитель выражения является посылкой, а знаменатель — заключением:
1)
2)
Правила следствия используются для доказательства сложных элементов программы. Пусть программа представлена в виде структуры (рис. 5.1), где Si — операторы, а Pi — предикаты, соответствующие дугам.
Рис. 5.1 — Структура программы
Предположим, что доказаны следующие утверждения: {P1}S1{P1'} и {P2}S2{P2'} для некоторых предикатов P1' и P2'. Если можно доказать, что P1' Þ P2 и P2' Þ P3, то, используя правила следствия, можно доказать, что {P1}S1;S2{P3} истинно.
Следует определить, какие операторы программы являются правильными. Предполагается, что программа состоит только из последовательности операторов присвоения и операторов if и do while.
Так как только оператор присвоения может изменять значение переменных, то для определения правильности оператора присвоения нужно добавить только одну аксиому, она называется аксиомой присвоения и формулируется следующим образом:
В соответствии с этой аксиомой устанавливается, что если P — утверждение, содержащее переменную x, истинно, то P должно быть истинно и до выполнения оператора присвоения, если x изменяется expr.
Например, если P(x) является предикатом x > 0 и x = x + 1 — оператор присвоения, то P(x + 1) является предикатом x + 1 > 0 или x > –1.
По правилам следствия, если можно доказать, что Q Þ P(x + 1) для некоторого предиката Q, то справедливо утверждение {Q}x = x + 1{x > 0} и предикат является предусловием для P.
Осталось определить правильные управляющие структуры. Введем следующие аксиомы.
Аксиома следования:
Два оператора программы могут быть объединены. Если после выполнения S1 предикат Q остается истинным и Q есть предусловие для оператора S2, то P является предусловием для операторов S1; S2.
Аксиома цикла:
Утверждается, что если истинность P не изменяется оператором S (т.е. является инвариантом), то P инвариантно относительно цикла, содержащего S. Кроме того, при выходе из цикла значение выражения B ложно.
Аксиома выбора:
а)
б)
Эти аксиомы устанавливают простые соотношения для оператора if.