Теорема определяет условия, при которых программа может быть выведена из спецификации.
Теорема 2.1 тождества спецификации и программы. Рассмотрим программу со спецификацией в виде тройки Хоара:
{P(x)} S {Q(x, y)} [7] . (2.15)
Допустим, оператор S является однозначным в области истинности предусловия P(x), а спецификация оператора S является реализуемой. Предположим, LS(S)(x, y) выводима из спецификации, т. е.
P(x) & Q(x, y) Þ LS(S)(x, y) . (2.16)
Тогда программа (2.15) является корректной.
Доказательство. Для доказательства корректности программы (2.15) достаточно доказать истинность формулы (2.10), т. е.
P(x) Þ [ LS(S)(x, y) Þ Q(x, y) ] & $y. LS(S)(x, y) .
Допустим, предусловие P(x) истинно.
Докажем истинность $y. LS(S)(x, y). Поскольку спецификация предиката S реализуема, то истинна формула $y. Q(x, y). Пусть эта формула истинна для некоторого y’. Тогда из (2.16) истинна LS(S)(x, y’) и, следовательно, $y. LS(S)(x, y).
Докажем истинность формулы LS(S)(x, y) Þ Q(x, y). Поскольку истинны P(x) и формула (2.16), то истинна формула Q(x, y) Þ LS(S)(x, y). В соответствии с леммой 2.7 истинна формула LS(S)(x, y) Þ Q(x, y), поскольку постусловие Q(x, y) реализуемо, а LS(S)(x, y) - однозначно. □
Лемма 2.8. В условиях теоремы 2.1 истинна следующая формула:
P(x) Þ (LS(S)(x, y) º Q(x, y)) .
Доказательство. Допустим, предусловие P(x) истинно. Истинность формулы LS(S)(x, y) Þ Q(x, y) установлена при доказательстве теоремы 2.1. Обратная импликация следует из (2.16). □
Как следствие леммы 2.8 спецификация в виде предусловия P(x) и постусловия Q(x, y) оказывается однозначной.
Лемма 2.9. Допустим, программа (2.15) является корректной, а ее спецификация - однозначной. Тогда истинна формула (2.16), т. е. LS(S)(x, y) выводима из спецификации.
Доказательство. Допустим, истинны P(x) и Q(x, y). Докажем истинность LS(S)(x, y).
Из корректности программы (2.15) по формуле (2.10) следует истинность формулы LS(S)(x, y) Þ Q(x, y), а также реализуемость LS(S)(x, y). Пусть для некоторого y’ истинно LS(S)(x, y’). Тогда истинно Q(x, y’), а из однозначности Q следует y = y’. Следовательно, истинно LS(S)(x, y). □
Теорема 2.1, сформулированная для программы в целом, применима также к произвольным операторам программы. Предлагаемая ниже система правил доказательства корректности операторов базируется на теореме 2.1, в соответствии с которой для реализуемой спецификации и при условии однозначности используемых операторов требуется доказать истинность формулы (2.16). Отметим, что однозначности спецификации не требуется. Однако в случае неоднозначной спецификации не удастся доказать истинность формулы (2.16).