Составители:
— предикаты,
— фигурные скобки,
— операторы языка программирования.
Формулы в ЛП называются тройкам и. Они и ме ют вид
{P } S {Q}, где P и Q — предикаты, определяющие отношения меж-
ду значениями переменных программы, а S — оператор или список
операторов.
(*) Интерпретация тройки. Тройка {P }S{Q} истинна при
условии, что если выполнение S начинается в состоянии, удовле-
творяющем P , и если в конце концов выполнение S завершается,
то результирующее состояни е удовлетворяет Q.
Эта интерпретация называется частичной корректностью (пра-
вильностью); харак терн ая черта частичной корректности в том, что
выполнение S может и не завершиться. Частичная корректность
относится к свойствам безопасности.
Тотальная (полная) корректн ость получается, если известно,
что S всегда завершается; это свойство относится к свойствам жи-
вучести.
Предикат P называется предусловием S, а предикат Q — по-
стусловием S.
Примером тройки, не обладающей свойством (*) служит такая
тройка
{x == 0} x = x + 1
| {z }
S
{y == 1}
Эта тройка не является истин ной, ибо операция S никак с y не
связана.
Аксиома присваивания: {P
x←e
} x = e {P }.
Запись P
x←e
означает текстуальную подстановку: заменить все
свободные вхождения x в предикат P выражением e (переменная
называется свободной в предикате, если она не входит в область
действия квантора существования или квантора всеобщности, име-
ющих переменную с тем же именем).
Эта аксиома означает: если нужно, чтобы присваивание при-
водило к п ред икату P , то предшествующее состояние должно удо-
влетворять предикату P , в котором вместо переменной x записано
выражение e.
30
Страницы
- « первая
- ‹ предыдущая
- …
- 27
- 28
- 29
- 30
- 31
- …
- следующая ›
- последняя »
