Page 56 - 4868

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

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

виконання програми завершиться. Відповідна властивість живучості – це
тотальна (повна) коректність, тобто часткова коректність плюс
завершуваність (всі історії закінчують своє виконання).
Предикати 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 , де
x e
запис P визначає текстуальну підстановку виду «замінити всі вільні
x e
входження змінної x в предикат P виразом e». Змінна називається вільною у
предикаті, якщо вона не входить в область дії квантора існування або
загальності, який має змінну з тим же іменем. Аксіома присвоєння говорить
про те, що якщо необхідно, щоб операція присвоєння породжувала стан, який
задовольняє предикату P , то попередній стан повинен задовольняти

предикату P , в якому замість змінної x записаний вираз e.
Як приклад для цієї аксіоми наведемо наступну трійку:
{1 == 1} x = 1; {x == 1}

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