Page 69 - 6571

Передумова спрощується до предиката true, яким характе-
ризуються всі стани. Таким чином, ця трійка означає, що, неза-
лежно від початкового стану, після присвоювання змінній x зна-

чення 1 отримується стан, що задовольняє предикату x == 1.
Більш загальний спосіб розгляду операції присвоєння можна
охарактеризувати фразою «йти вперед», тобто розгляд почина-

ється з деякого предиката, що характеризує поточний стан, а по-
тім записується предикат, істинний для стану, що отримується
після виконання операції присвоєння. Наприклад, якщо почати в
стані, в якому x == 0, і додати 1 до x, то в результуючому стані

значенням змінної x буде 1. Ця операція описується наступною
трійкою

{x == 0} x = 1; {x == 1}.

Аксіома присвоєння описує зміну стану. Правила виведення
в такій логіці програмування дозволяють поєднувати теореми,

отримані з окремих випадків аксіоми присвоєння. Зокрема, пра-
вила виведення використовуються для опису композиції операто-
рів (списків операторів) і операторів керування, наприклад if та

while. Вони також дозволяють змінювати предикати в трійках.
На рисунку 8.1 представлені чотири найбільш важливих пра-
вила виведення. Правило композиції дозволяє склеїти трійки для

двох операторів, виконуваних один за одним. Перша гіпотеза в
правилі оператора if характеризує результат виконання опера-
тора S, коли умова істинна; другий описує, що є істинно, якщо B
хиба. Як простий приклад використання цих правил розглянемо

програму, яка присвоює змінній m максимальне із значень x та y.

{true} m = x; {m == x}
if (y > m) m = y;
{(m == xÙm >= y) or (m == y)Ùm > x)}

При будь-якому початковому стані перше присвоєння приз-
водить до стану, коли m == x. Після виконання оператора if

значення змінної m рівне x і не менше y, або воно рівне y і не
більше за x.

{ }P S { }, { }Q Q S { }R
Правило композиції 1 2
;
{ }P S S 2 { }R
1

68