Page 57 - 4868

55 Ошибка! Стиль не определен.

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

наступною трійкою
{x == 0} x = 1; {x == 1}.

Аксіома присвоєння описує зміну стану. Правила виведення в такій
логіці програмування дозволяють поєднувати теореми, отримані з окремих
випадків аксіоми присвоєння. Зокрема, правила виведення використовуються
для опису композиції операторів (списків операторів) і операторів керування,
наприклад if та while. Вони також дозволяють змінювати предикати в
трійках.
На рисунку 1.14 представлені чотири найбільш важливих правила
виведення. Правило композиції дозволяє склеїти трійки для двох операторів,
виконуваних один за одним. Перша гіпотеза в правилі оператора 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 { }R
1 2
{P  B } S { }, {Q P   B } Q
Правило оператора if
{ }P if ( ) ; { }B S Q

{I  B } S { }I
Правило оператора while
{ }I while ( ) ;{B S I   B }
{P  P }, { }P S { },Q Q  Q
Правило слідування

{ }P S { }Q
Рисунок 1.14 – Правила виведення в логіці програмування

Для правила оператора while необхідний інваріант циклу I
.Інваріантом називається предикат (логічний вираз), значення якого «істина»
перед кожним повторенням циклу і після нього. Якщо інваріант I і умова
циклу B істинні перед виконанням тіла циклу S , то виконання S повинно
знову зробити істинним I . Таким чином, коли оператор циклу завершується,
інваріант I залишається істинним, а B стає хибним. Як приклад наведемо

наступну програму, яка переглядає масив a і шукає в ньому перше