Логика Хоара¶

Логика Хоара — это формальная система, предназначенная для верификации императивных компьютерных программ. Она была предложена британским учёным Чарльзом Энтони Ричардом Хоаром (C. A. R. Hoare) в 1969 году. Логика Хоара позволяет математически строго доказывать корректность программ, то есть устанавливать, что выполнение программы при соблюдении определённых предусловий обязательно приводит к заданным постусловиям, при этом программа не содержит ошибок времени выполнения (например, деления на ноль). В основе логики лежит понятие тройки Хоара — утверждения о состоянии программы до и после выполнения фрагмента кода.

¶Основные понятия

¶Тройка Хоара

Центральным элементом логики Хоара является тройка Хоара, которая записывается в виде: \[ \{P\}\ C\ \{Q\} \] где:

• \(P\) — предусловие (логическое утверждение о состоянии памяти до выполнения команды \(C\));
• \(C\) — команда (фрагмент императивной программы);
• \(Q\) — постусловие (логическое утверждение о состоянии памяти после выполнения команды \(C\)).

Семантически тройка \(\{P\}\ C\ \{Q\}\) означает: если перед выполнением команды \(C\) истинно предусловие \(P\), то после завершения \(C\) (если оно вообще происходит) будет истинно постусловие \(Q\). При этом предполагается, что выполнение команды завершается (то есть не происходит зацикливания). Для учёта частичной корректности (когда завершение не гарантируется) используется тройка без этого требования; полная корректность требует доказательства завершения.

¶Частичная и полная корректность

Различают два типа корректности:

• Частичная корректность: если программа завершается, то её результат удовлетворяет спецификации. Для доказательства частичной корректности достаточно показать, что из истинности предусловия следует истинность постусловия после выполнения, при условии, что программа завершается.
• Полная корректность: программа обязательно завершается, и её результат удовлетворяет спецификации. Доказательство полной корректности требует дополнительно показать, что программа не зацикливается (обычно с помощью инвариантов и обоснования завершения циклов).

¶Аксиомы и правила вывода

Логика Хоара строится на наборе аксиом и правил вывода, которые позволяют выводить тройки для составных команд из троек для простых команд. Основные правила:

¶Аксиома пропуска (skip)

Для пустой команды, которая ничего не делает: \[ \{P\}\ \text{skip}\ \{P\} \] Выполнение skip не меняет состояние, поэтому постусловие совпадает с предусловием.

¶Аксиома присваивания

Для команды присваивания \(x := E\) (где \(E\) — выражение): \[ \{P[E/x]\}\ x := E\ \{P\} \] Здесь \(P[E/x]\) означает замену всех свободных вхождений переменной \(x\) в утверждении \(P\) на выражение \(E\). Правило читается так: если после присваивания мы хотим, чтобы выполнялось \(P\), то до присваивания должно выполняться \(P\) с заменённой переменной.

¶Правило последовательности

Для двух команд \(C_1\) и \(C_2\), выполняемых последовательно: \[ \frac{\{P\}\ C_1\ \{R\},\quad \{R\}\ C_2\ \{Q\}}{\{P\}\ C_1; C_2\ \{Q\}} \] Если первая команда переводит состояние из \(P\) в \(R\), а вторая — из \(R\) в \(Q\), то их последовательность переводит из \(P\) в \(Q\).

¶Правило условного оператора

Для условной конструкции if \(B\) then \(C_1\) else \(C_2\): \[ \frac{\{P \land B\}\ C_1\ \{Q\},\quad \{P \land \lnot B\}\ C_2\ \{Q\}}{\{P\}\ \text{if } B \text{ then } C_1 \text{ else } C_2\ \{Q\}} \] Если при истинности условия \(B\) команда \(C_1\) из состояния \(P \land B\) приводит к \(Q\), а при ложности \(B\) команда \(C_2\) из \(P \land \lnot B\) приводит к \(Q\), то весь условный оператор из \(P\) приводит к \(Q\).

¶Правило цикла while

Для цикла while \(B\) do \(C\): \[ \frac{\{I \land B\}\ C\ \{I\}}{\{I\}\ \text{while } B \text{ do } C\ \{I \land \lnot B\}} \] Здесь \(I\) — инвариант цикла — утверждение, которое остаётся истинным на каждой итерации. Правило означает: если выполнение тела цикла \(C\) сохраняет инвариант \(I\) при условии, что \(B\) истинно, то после завершения цикла (когда \(B\) становится ложным) будет истинно \(I \land \lnot B\). Для полной корректности дополнительно требуется доказать, что цикл завершается (например, с помощью варианта — целочисленной функции, строго убывающей на каждой итерации и ограниченной снизу).

¶Правило консеквенции (ослабления)

Позволяет усиливать предусловие или ослаблять постусловие: \[ \frac{P \Rightarrow P',\quad \{P'\}\ C\ \{Q'\},\quad Q' \Rightarrow Q}{\{P\}\ C\ \{Q\}} \] Если из \(P\) следует \(P'\), а из \(Q'\) следует \(Q\), то можно заменить предусловие на более сильное, а постусловие — на более слабое.

¶Применение

¶Верификация программ

Логика Хоара используется для формального доказательства корректности программ. Программа разбивается на блоки, для каждого блока формулируется тройка, и с помощью правил вывода строится доказательство. Особенно важна роль инвариантов циклов, которые часто являются наиболее сложной частью верификации.

¶Автоматизация и инструменты

На основе логики Хоара разработаны инструменты автоматической верификации, такие как:

• Why3 — платформа для дедуктивной верификации программ на языках C, Java, OCaml и других.
• Frama-C — статический анализатор для C-программ, использующий логику Хоара для проверки контрактов (предусловий, постусловий, инвариантов).
• Dafny — язык программирования со встроенной поддержкой верификации на основе логики Хоара.
• SPARK — подмножество языка Ada, ориентированное на формальную верификацию.

¶Обучение и теория

Логика Хоара является фундаментальной частью курсов по формальным методам, теории программирования и верификации. Она лежит в основе семантики императивных языков и используется для доказательства свойств программ, таких как безопасность (отсутствие ошибок времени выполнения) и функциональная корректность.

¶Ограничения и критика

Несмотря на свою мощь, логика Хоара имеет ряд ограничений:

• Сложность инвариантов: для реальных программ подбор инвариантов циклов может быть нетривиальной задачей, требующей глубокого понимания алгоритма.
• Неполнота для недетерминированных и параллельных программ: классическая логика Хоара не учитывает параллелизм и недетерминизм. Для верификации параллельных программ были разработаны расширения, такие как логика разделения (separation logic) и логика для параллельных систем (например, Owicki–Gries).
• Проблема завершения: доказательство полной корректности требует обоснования завершения циклов, что для сложных рекурсивных или итеративных алгоритмов может быть сложно.
• Масштабируемость: ручное доказательство корректности больших программ трудоёмко, а автоматические инструменты не всегда справляются с программами промышленного масштаба.

¶История и развитие

Логика Хоара была впервые представлена в статье «An Axiomatic Basis for Computer Programming» (1969). Она стала развитием идей Роберта Флойда, который ранее предложил метод индуктивных утверждений для блок-схем. Впоследствии логика была расширена и обобщена:

• Логика разделения (Separation Logic) — добавлена поддержка указателей и динамической памяти, что позволило верифицировать программы с кучей.
• Логика для объектно-ориентированных программ — адаптация для классов, наследования и полиморфизма.
• Логика для параллельных и распределённых систем — введение понятий глобальных и локальных состояний, а также синхронизации.

¶Пример

Рассмотрим простой пример: программа, вычисляющая факториал числа \(n\) (предполагается, что \(n \ge 0\)): `` x := 1; i := 0; while i < n do i := i + 1; x := x * i `` Требуется доказать, что после выполнения программы \(x = n!\). Предусловие: \(n \ge 0\). Постусловие: \(x = n!\). Инвариант цикла: \(x = i! \land i \le n\). Доказательство:

1. После инициализации \(x=1\), \(i=0\): \(x = 0! = 1\), инвариант выполнен.
2. Тело цикла: при \(i < n\) выполняется \(i := i+1; x := xi\). Если до итерации \(x = i!\) и \(i < n\), то после \(i' = i+1\) и \(x' = x i' = i! * (i+1) = (i+1)! = i'!\). Инвариант сохраняется.
3. После завершения цикла \(i = n\) (так как условие \(i < n\) ложно), и из инварианта \(x = i!\) получаем \(x = n!\). Постусловие выполнено.

¶Источники

• C. A. R. Hoare. «An Axiomatic Basis for Computer Programming». Communications of the ACM, 1969.
• Glynn Winskel. «The Formal Semantics of Programming Languages». MIT Press, 1993.
• John C. Reynolds. «Theories of Programming Languages». Cambridge University Press, 1998.
• K. Rustan M. Leino. «Dafny: An Automatic Program Verifier for Functional Correctness». LPAR, 2010.