Page 68 - 6571

тивість живучості – це тотальна (повна) коректність, тобто час-
ткова коректність плюс завершуваність (всі історії закінчують
своє виконання).
Предикати P та Q в трійці часто називаються твердженнями,

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

дикат P називається передумовою S. Він описує умову, якій має
задовольняти стан перед початком виконання S. Предикат Q на-
зивається післяумовою S. Він описує стан після виконання S за

умови, що виконання S завершується. Двома особливими твер-
дженнями є true (істина), що характеризує всі стани програми, і
false (хиба), яке не описує жодного стану програми.

Для того щоб інтерпретація могла виступати моделлю логіки
програмування, аксіоми і правила виведення ЛП повинні бути не-
суперечливими. Це гарантує, що всі доказові теореми в ЛП несу-
перечливі. Наприклад, дана трійка є теоремою:

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

Однак наступна трійки не буде теоремою, оскільки процеду-

ра присвоєння значення змінній x не може змінити значення
змінної y на 1:

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

Найважливішою аксіомою логіки програмування є аксіома,
пов’язана із операцією присвоєння.

Аксіома присвоєнняформально представляється як
{P } x = e { }P , де запис P визначає текстуальну підстано-
x¬ e x¬ e
вку виду «замінити всі вільні входження змінної x в предикат P

виразом e». Змінна називається вільною у предикаті, якщо вона
не входить в область дії квантора існування або загальності, який

має змінну з тим же іменем. Аксіома присвоєння говорить про те,
що якщо необхідно, щоб операція присвоєння породжувала стан,
який задовольняє предикату P, то попередній стан повинен
задовольняти предикату P, в якому замість змінної x записаний

вираз e.
Як приклад для цієї аксіоми наведемо наступну трійку:

{1 == 1} x = 1; {x == 1}

67