Page 67 - 6571

суперечливе, якщо його наслідок відображається в істину, за
умови, що всі його гіпотези відображаються в істину. Отже, якщо
логіка несуперечлива, то всі теореми є істинними твердженнями
в розглянутій області. У такому випадку інтерпретація називаєть-

ся моделлю логіки.
Поняття повноти дуально поняттю несуперечності. Логіка є
повною щодо інтерпретації, якщо формула, яка відображається в

істину, є теоремою, тобто в даній логіці доказова будь-яка (дійс-
на) формула. Таким чином, якщо ФАКТИ – це множина істинних
тверджень, що виражаються формулами логіки, а ТЕОРЕМИ –
множина теорем логіки, то несуперечність означає, що ТЕОРЕ-

МИ Í ФАКТИ, а повнота – ФАКТИ Í ТЕОРЕМИ. Повна і несу-
перечлива логіка дозволяє довести всі її істинні твердження.

8.2 Логіка програмування

Отже, логіка програмування є формальною логічною систе-
мою, яка дозволяє встановлювати і обґрунтовувати (доводити)
властивості програм.

Як і в будь-якій формальній логічній системі, в ЛП визначені
символи, формули, аксіоми і правила виведення. Символи ЛП –
це предикати, фігурні дужки і оператори мови програмування.

Формули в ЛП називаються трійками. Вони мають наступний
вигляд:

{ } { }P S Q ,

де предикати P та Q визначають відношення між значеннями
змінних програми, а S – оператор або список операторів.
Ціль логіки програмування полягає в тому, щоб забезпечити
можливість обґрунтовувати (доводити) властивості виконання

програми. Отже, інтерпретація трійки характеризує відношення
між предикатами P та Q і списком операторів S.
Трійка { } { }P S Q істинна за умови, якщо виконання програми

починається в стані, що задовольняє P, завершується успішно і
результуючий стан задовольняє Q.

Ця інтерпретація називається частковою коректністю, яка є
властивістю безпеки. Вона стверджує, що якщо початковий стан
програми задовольняє P, то результуючий стан задовольнятиме Q
за умови, що виконання програми завершиться. Відповідна влас-

66