Page 70 - 6571

{P Ù B } { }, {S Q P Ù Ø }⇒ Q
B
Правило оператора 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 ¢
¢
Рисунок 8.1 – Правила виведення в логіці програмування
Для правила оператора while необхідний інваріант циклу I .

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

ким чином, коли оператор циклу завершується, інваріант I зали-
шається істинним, а стає хибним. Як приклад наведемо насту-
B
пну програму, яка переглядає масив a і шукає в ньому перше

входження значення x. За умови, що x зустрічається в a, цикл за-
вершується присвоєнням змінній i індексу першого входження.

i = 1;
{i == 1 Ù ("j: 1 <= j < і:a[j] != x)}
while (a[і] != x)
і = і+1;
{("j:1 <= j < і:a[j] != x) Ù a[i] == x}

В даному прикладі інваріантом циклу виступає предикат з
квантором. Він істинний перед виконанням циклу, оскільки об-

ласть визначення квантора порожня. Він також істинний перед
кожним виконанням тіла циклу і після нього. Коли виконання
оператора циклу завершується, a[1] рівно x, і значення x раніше

не зустрічалося в масиві a.
Правило слідування дозволяє посилювати передумови і пос-
лаблювати постумови. В якості прикладу розглянемо наступну

трійку:

{x == 0} x = x+1; {x == 1}

Згідно правила слідування істинною буде також наступна
трійка:

{x == 0} x = x+1; {x> 0}

69