Рассмотрим программу с предикатной спецификацией на языке, для которого можно построить логическую семантику. Программа со спецификацией представляется в виде тройки Хоара:
{P(x)} S {Q(x, y)} . (2.5)
Здесь программа представлена оператором S, x - набор входных данных, y - набор результатов.
Закон соответствия программы и спецификации, сформулированный в разд. 2.1, очевидным образом конкретизируется для программы с предикатной спецификацией в виде следующих условий:
· входные данные x должны соответствовать предусловию P(x) перед исполнением программы;
· входные данные x и результаты y должны удовлетворять постусловию Q(x, y) после завершения исполнения программы.
Во втором условии неявно подразумевается, что исполнение программы на входных данных x завершается. Более точная формулировка условия: если для набора x существует исполнение, завершающееся набором y, то истинно постусловие Q(x, y). Используя обозначения, введенные в разд. 2.2, запишем условие в виде формулы: RUN(S, x, y) Þ Q(x, y). Учитывая свойство согласованности (2.4), второе условие можно представить формулой: LS(S)(x, y) Þ Q(x, y). В итоге, закон соответствия программы и спецификации для программы с предикатной спецификацией выражается следующей формулой:
P(x) & ( LS(S)(x, y) Þ Q(x, y) ) . (2.6)
Замечание. Импликация в обратную сторону, т. е. Q(x, y) Þ LS(S)(x, y), в общем случае неверна. Во многих задачах спецификация Q(x, y) представляется более слабым (общим) условием, допускающим для фиксированного набора x не единственное решение y.
Предусловие P(x) не зависит от оператора S, поскольку значение P(x) определено до исполнения оператора S. Для программы в целом предусловие P(x) считается истинным априори. Истинность предусловия для случая, когда оператор S является частью программы, должна быть доказана, см. разд. 2.4 и 2.5. В любом случае, исполнение оператора S не рассматривается для ложного предусловия. Таким образом, истинность предусловия P(x) определяется как необходимое условие для тройки Хоара (2.5).
Закон соответствия программы и спецификации (2.6) определяет условие корректности программы (2.5). Однако первый конъюнкт P(x) не может входить в условие корректности оператора S, а второй конъюнкт реализуется при условии истинности P(x). Учитывая это, условие корректности программы представляется следующей формулой:
P(x) & LS(S)(x, y) Þ Q(x, y) . (2.7)
Предикат H(x, y) реализуем для конкретного x, если H(x, y) истинен для некоторого y, т. е. $y. H(x, y). Предикат H(x, y) реализуем в области предусловия P(x), если он реализуем для всех x, на которых истинно предусловие, т. е. "x. (P(x) Þ $y. H(x, y)). Предикат H(x, y) является тотальным в области предусловия, если рассматривать его как функцию, отображающую x в y. Спецификация в виде предусловия P(x) и постусловия Q(x, y) реализуема, если постусловие реализуемо в области предусловия.
Рассмотрим ситуацию, когда условие корректности (2.7) истинно, а спецификация нереализуема. Тогда для некоторого x истинно предусловие P(x), а постусловие Q(x, y) ложно для всех y. Из истинности (2.7) следует, что LS(S)(x, y) будет ложной для всех y. Как следствие свойства согласованности (2.4) получим, что "y ØRUN(S, x, y) истинно, т. е. исполнение оператора S для данного x не определено. Это означает, что исполнение либо реализуется бесконечно, либо завершается аварийно без получения результата. Подобная ситуация абсурдна в модели применения программы (см. рис. 1) – такое исполнение бессмысленно и не соответствует цели базового процесса.
Таким образом, мы приходим к следующему условию корректности спецификации: спецификация должна быть реализуема, т. е.:
P(x) Þ$y. Q(x, y) . (2.8)
Корректность спецификации является необходимым условием корректности программы, представленной тройкой (2.5).
Определим точное предусловие [6] PE(x) следующей формулой:
PE(x) @ $y. Q(x, y) .
Лемма 2.1. Спецификация с предусловием P(x) и постусловием Q(x, y) реализуема Û P(x) Þ PE(x).
Ситуация, когда для некоторого набора x, удовлетворяющего предусловию P(x), исполнение оператора S реализуется бесконечно или завершается аварийно без получения результата, т. е. "y. ØRUN(S, x, y), определена выше как недопустимая для программы с предикатной спецификацией. Следовательно, должно быть истинно обратное утверждение: $y. RUN(S, x, y), т. е. исполнение программы завершается с получением некоторого результата y. Данное утверждение эквивалентно $y. LS(S)(x, y), что следует из свойства согласованности (2.4). Таким образом, необходимым условием корректности программы является нормальное завершение исполнения программы для x, удовлетворяющего предусловию P(x). Условие корректности определяется формулой:
P(x) Þ $y. LS(S)(x, y) . (2.9)
Приведенные выше требования объединим в понятии корректности программы. Прежде всего, для программы (2.5) предусловие P(x) всегда истинно. Программа корректна, если спецификация реализуема (условие (2.8)), программа нормально завершается в области предусловия (условие (2.9)) и программа соответствует спецификации (условие (2.7)).
Требования, составляющие корректность программы, избыточны.
Лемма 2.2. Если программа соответствует спецификации и нормально завершается в области предусловия, то спецификация реализуема.
Доказательство. Пусть истинно P(x). Необходимо доказать истинность $y. Q(x, y). Из условия (2.9) следует истинность $y. LS(S)(x, y). Допустим, истинность этой формулы реализуется для некоторого y0. Из условия (2.7) получаем истинность Q(x, y0), а значит – и $y. Q(x, y). □
Таким образом, корректность программы (2.5) определяется двумя условиями: соответствие спецификации (2.7) и нормального завершения (2.9). Объединяя формулы (2.7) и (2.9), получаем итоговую формулу корректности программы:
P(x) Þ [ LS(S)(x, y) Þ Q(x, y) ] & $y. LS(S)(x, y) . (2.10)
Приведенное определение корректности программы соответствует общеизвестному понятию тотальной (или полной) корректности программы. Оно справедливо для программ с предикатной спецификацией и для языков программирования с логической семантикой. Основой данного определения корректности является формализация закона соответствия программы и спецификации для программ с предикатной спецификацией.