Философия
Дейкстра отвергал традиционный цикл "написать → проверить → исправить". Его подход — конструировать доказательство вместе с кодом, а не искать ошибки постфактум. Программа строится из спецификации через цепочку формальных преобразований, где каждый шаг гарантированно корректен.[sciencedirect]
Weakest Precondition Calculus (wp)
Дейкстра разработал метод слабейших предусловий (weakest precondition) — механический способ вывести, что должно быть истинно до выполнения команды, чтобы после гарантировать желаемое состояние.[en.wikipedia]
Определение: Для программы SSS и постусловия RRR, слабейшее предусловие wp(S,R)wp(S, R)wp(S,R) — это самое слабое (наименее ограничивающее) условие QQQ, при котором выполнение SSS гарантирует RRR.[moves.rwth-aachen]
Формально: P⇒wp(S,R)P \Rightarrow wp(S, R)P⇒wp(S,R) тогда и только тогда, когда {P}S{R}\{P\} S \{R\}{P}S{R} — валидная тройка Хоара.[moves.rwth-aachen]
Пример: присваивание
Для присваивания x := E и постусловия QQQ:
wp(x := E,Q)=Q[x/E]wp(\text{x := E}, Q) = Q[x/E]wp(x := E,Q)=Q[x/E]
То есть: заменить все xxx в QQQ на выражение EEE.[cs.umd]
Конкретный случай:
textПостусловие: { x == 1 }
Команда: x := y
Предусловие: { y == 1 } // заменили x на y
Пример: последовательность команд
Дейкстра работает назад от желаемого результата:[cs.umd]
textЦель: { z == 6 } // (5) финальное постусловие
z := x - y // (4) { x - y == 6 }
y := x - y // (3) { x - (x - y) == 6 } → { y == 6 }
x := x - y // (2) { (x - y) - y == 6 } → { x == 2y + 6 }
На каждом шаге мы механически подставляем правую часть присваивания вместо переменной в постусловии.[moves.rwth-aachen]
Композиция программ
Для последовательности C1;C2C_1; C_2C1;C2 и постусловия FFF:
wp(C1;C2,F)=wp(C1,wp(C2,F))wp(C_1; C_2, F) = wp(C_1, wp(C_2, F))wp(C1;C2,F)=wp(C1,wp(C2,F))
Сначала находим wp(C2,F)wp(C_2, F)wp(C2,F) — это становится постусловием для C1C_1C1.[moves.rwth-aachen]
Недетерминизм
Для выбора {C1} □ {C2} (один из них выполнится):
wp({C1}□{C2},F)=wp(C1,F)∧wp(C2,F)wp(\{C_1\} \square \{C_2\}, F) = wp(C_1, F) \land wp(C_2, F)wp({C1}□{C2},F)=wp(C1,F)∧wp(C2,F)
Предусловие должно гарантировать FFF независимо от того, какая ветка выполнится.[moves.rwth-aachen]
Практическое применение
Дейкстра использовал этот метод для построения многопоточных систем (producer-consumer с семафорами). Вместо написания кода и отладки race conditions, он вывел корректную программу из спецификации через цепочку wp-преобразований.[cs.utexas]
Результат: программа корректна по построению, не требует тестирования логики (только проверку соответствия спецификации реальности).[stringology]
Хоар: Логика и контракты
Тройка Хоара
Базовая форма:
{P} C {Q}\{P\} \, C \, \{Q\}{P}C{Q}
- PPP — предусловие (что истинно до CCC)
- CCC — команда (код)
- QQQ — постусловие (что истинно после CCC)
Значение: "Если PPP истинно перед выполнением CCC, то после завершения CCC будет истинно QQQ".[en.wikipedia]
Правила вывода
Присваивание:
{Q[x/E]} x:=E {Q}\frac{}{\{Q[x/E]\} \, x := E \, \{Q\}}{Q[x/E]}x:=E{Q}
[en.wikipedia]
Последовательность:
{P}C1{R}{R}C2{Q}{P}C1;C2{Q}\frac{\{P\} C_1 \{R\} \quad \{R\} C_2 \{Q\}}{\{P\} C_1; C_2 \{Q\}}{P}C1;C2{Q}{P}C1{R}{R}C2{Q}
Промежуточное состояние RRR связывает команды.[en.wikipedia]
Условный оператор:
{P∧B}C1{Q}{P∧¬B}C2{Q}{P}if B then C1 else C2{Q}\frac{\{P \land B\} C_1 \{Q\} \quad \{P \land \neg B\} C_2 \{Q\}}{\{P\} \text{if } B \text{ then } C_1 \text{ else } C_2 \{Q\}}{P}if B then C1 else C2{Q}{P∧B}C1{Q}{P∧¬B}C2{Q}
В каждой ветке можно использовать знание об условии BBB.[cs.umd]
Усиление/ослабление (Rule of Consequence):
{P′}C{Q′}P⇒P′Q′⇒Q{P}C{Q}\frac{\{P'\} C \{Q'\} \quad P \Rightarrow P' \quad Q' \Rightarrow Q}{\{P\} C \{Q\}}{P}C{Q}{P′}C{Q′}P⇒P′Q′⇒Q
Можно усилить предусловие (PPP сильнее P′P'P′) или ослабить постусловие (QQQ слабее Q′Q'Q′).[cs.umd]
Hoare State Monad
Это монада, где состояние SSS сопровождается предикатами PPP и QQQ:[microsoft]
haskelldata HoareState s a = HS {
runHS :: s -> (a, s),
pre :: s -> Bool, -- предусловие
post :: s -> a -> s -> Bool -- постусловие
}
При композиции монад предикаты автоматически проверяются через систему типов:[microsoft]
haskell(>>=) :: HoareState s a -> (a -> HoareState s b) -> HoareState s b
Компилятор генерирует verification conditions — условия, которые нужно доказать, чтобы программа была корректна.[microsoft]
Программа = устройство с контрактами
Каждая функция — это "компонент" с гарантиями:
- Требует (precondition): что клиент должен обеспечить
- Обеспечивает (postcondition): что компонент гарантирует взамен
Это как электрический разъём: вход 220В ± 10% → выход 12В ± 0.5В.[en.wikipedia]
Сравнение подходов
АспектДейкстра (wp)Хоар (тройки)НаправлениеНазад от цели [cs.utexas]Вперёд от начала [en.wikipedia]ФокусКонструирование программы [sciencedirect]Верификация готового кода [en.wikipedia]АвтоматизацияМеханическое вычисление wp [en.wikipedia]Требует доказательства каждого шага [en.wikipedia]ПрактичностьДля малых алгоритмов [cs.utexas]Для спецификации больших систем [en.wikipedia]
Дейкстра критиковал Хоара за то, что его логика применяется после написания кода — это "debugging with proof", а не "construction with proof". Дейкстра требовал: пока не доказал — не пиши код.[arxiv]