Главная Случайная страница Контакты | Мы поможем в написании вашей работы! | ||
|
Рассмотрим спецификацию оператора суперпозиции в виде тройки Хоара:
{P(x)} A; B {Q(x, y)} [9]. (2.18)
Предположим, что операторы A и B корректны. Их спецификации представлены тройками:
{PA(x)} A {QA(x, z)}, {PB(z)} B {QB(z, y)}.
Определим правила, гарантирующие корректность оператора суперпозиции (2.18).
Правило LS1. P(x) ├ PA(x).
Правило LS2. P(x) & Q(x, y) & QA(x, z) ├ PB(z) & QB(z, y).
Лемма 2.11. Допустим, спецификация оператора суперпозиции (2.18) реализуема, операторы A и B однозначны в области предусловий и корректны, а их спецификация B однозначна. Если правила LS1 и LS2 истинны, то оператор суперпозиции (2.18) является корректным.
Доказательство. Поскольку операторы A и B однозначны, то и оператор суперпозиции (2.18) является однозначным. В соответствии с теоремой 2.1 для доказательства леммы достаточно доказать истинность формулы:
P(x) & Q(x, y) Þ LS(A; B)(x, y).
В соответствии с (2.1) формула LS(A; B)(x, y) эквивалентна $z.(LS(A)(x, z) & LS(B)(z, y)).
Пусть истинны P(x) и Q(x, y). Докажем истинность $z.(LS(A)(x, z) & LS(B)(z, y)). Из истинности предусловия P(x) по правилу LS1 следует истинность PA(x). Из корректности оператора A следует истинность формул $z. LS(A)(x, z) и LS(A)(x, z) Þ QA(x, z). Допустим для некоторого z0 истинно LS(A)(x, z0). Тогда истинно QA(x, z0). В соответствии с правилом LS2 истинна формула PB(z0) & QB(z0, y). В соответствии с леммой 2.9 истинна формула
PB(z) & QB(z, y) Þ LS(B)(z, y).
Тогда истинна LS(B)(z0, y). В итоге, будет истинна формула $z.(LS(A)(x, z) & LS(B)(z, y)). □
Дата публикования: 2014-11-18; Прочитано: 225 | Нарушение авторского права страницы | Мы поможем в написании вашей работы!