Аксиоматическая семантика и Hoare Logic

Therac-25. 1985-1987. Радиационный аппарат для лечения рака убил 6 пациентов из-за race condition в C коде. Если бы Hoare Logic применялась для верификации медицинского ПО - эти смерти можно было предотвратить. Это не история. Это аргумент.

• **seL4** (NICTA/CSIRO, 2009): первое в мире формально верифицированное OS ядро - 8700 строк C, доказательство корректности 200 000 строк Isabelle/HOL. Используется в военных беспилотниках и медицинских устройствах
• **Amazon Web Services**: TLA+ для верификации алгоритмов DynamoDB (replikation protocol), S3 (consistency), EC2 (storage virtualization). 10+ лет практического применения
• **Microsoft Dafny**: язык с встроенной верификацией через Hoare Logic, активно используется в Azure SDK для критических компонентов. VS Code extension показывает verification errors в реальном времени

Предусловия: что должно быть верно до выполнения

1969 год. Тони Хоар публикует 'An Axiomatic Basis for Computer Programming'. 16 страниц. Эта работа определила как мы думаем о корректности программ на следующие 50 лет. Центральная идея: программу можно описать через логические утверждения о её поведении, а не через её выполнение.

Предусловие - логическое утверждение о состоянии программы, которое должно быть истинным **перед** выполнением операции. Нотация: `{P} C {Q}` - тройка Хоара. P - предусловие, C - команда, Q - постусловие. Читается: 'если P истинно до C, то Q истинно после C'. Это частичная корректность - не гарантирует завершения.

Design by Contract (Бертран Мейер, Eiffel, 1986) - практическая реализация Hoare Logic: preconditions (require), postconditions (ensure), invariants (invariant). Rust trait bounds - статическая форма предусловий, проверяемых компилятором. AWS формально верифицирует критические части S3 и EC2 используя TLA+ - похожий подход на уровне систем.

Постусловия: что гарантирует программа

Правила вывода в Hoare Logic позволяют строить доказательства корректности снизу вверх. Правило присваивания: `{Q[x:=E]} x := E {Q}`. Чтобы получить Q после присваивания, нужно Q с заменой x на E до. Правило следования: `{P} C1 {Q}` и `{Q} C2 {R}` дают `{P} C1; C2 {R}`.

Hoare Logic легла в основу формальной верификации программного обеспечения. SeL4 - формально верифицированный микроядро ОС (2009): 8700 строк C, доказательство корректности 200 000 строк Isabelle/HOL. Используется в drone firmware и медицинских устройствах. Amazon использует TLA+ для верификации протоколов распределённых систем (DynamoDB consistency, S3 replication).

Инварианты циклов: ключ к верификации итерации

Циклы - самая сложная часть верификации. Правило для while: если I - инвариант цикла (истинно до, в процессе и после), то из `{I ∧ B} body {I}` следует `{I} while B do body done {I ∧ ¬B}`. Придумать правильный инвариант - это искусство. Слишком слабый - не доказывает нужное. Слишком сильный - невозможно доказать, что он выдерживается.

Автоматический поиск инвариантов - активная область исследований. Daikon (MIT) извлекает инварианты из трасс выполнения. Code2Inv (нейросетевой подход, 2019) использует GNN для предсказания инвариантов. GitHub Copilot может предлагать инварианты в Dafny - хотя надёжность ещё далека от production.

Weakest Precondition Calculus: автоматизация верификации

Эдсгер Дейкстра (1975) формализовал WP (Weakest Precondition): wp(C, Q) - наислабейшее предусловие, из которого C гарантирует Q. 'Наислабейшее' значит: самое общее, допускающее максимум начальных состояний. Если наше фактическое предусловие P влечёт wp(C, Q), то {P} C {Q} верно.

WP calculus механически вычислим для большинства конструкций. wp(x := E, Q) = Q[x:=E]. wp(C1; C2, Q) = wp(C1, wp(C2, Q)). wp(if B then C1 else C2, Q) = (B → wp(C1,Q)) ∧ (¬B → wp(C2,Q)). Только цикл требует инвариант. Это основа современных program verifiers.

Связанные темы

Аксиоматическая семантика связывает логику с программированием:

• Денотационная семантика — Математическая база, на которой строится Hoare Logic
• Property Testing — Empirical альтернатива формальной верификации для практики
• Theorem Provers — Автоматизация доказательств Hoare Logic через Isabelle, Coq, Lean

Ключевые идеи

• **Тройка Хоара** {P} C {Q}: если P истинно до C, то Q истинно после (частичная корректность). Правила вывода для каждой конструкции.
• **Правило присваивания**: {Q[x:=E]} x:=E {Q}. Предусловие = постусловие с подстановкой. Механическое backward reasoning.
• **Инварианты циклов**: наиболее сложная часть. I сохраняется через итерации. Автоматический поиск - активная исследовательская область.
• **WP Calculus** (Дейкстра): wp(C,Q) - наислабейшее предусловие. Механически вычислимо для всех конструкций кроме цикла. Основа современных verifiers.

Вопросы для размышления

• Hoare Logic доказывает частичную корректность - не гарантирует завершения. Как доказать что программа завершается (total correctness)?
• SMT solvers (Z3) автоматически проверяют условия верификации Hoare Logic. Где граница автоматизации и где всё ещё нужен человек?
• Design by Contract в Eiffel vs типовая система Rust vs Hoare Logic: как эти три подхода к корректности соотносятся по мощности и удобству?

Связанные уроки

• plt-15-denotational-semantics — Денотационная семантика - математическая база для Hoare Logic
• plt-35-theorem-provers — Hoare Logic - фундамент автоматизированных theorem provers (Dafny, Frama-C)
• plt-34-property-testing — Property testing и Hoare Logic - два подхода к верификации корректности
• plt-33-model-checking — Model checking - дополнительный метод верификации наряду с Hoare Logic
• logic-32-natural-deduction