Слабейшее предусловие

Слабейшее предусловие — это в информатике и формальной верификации программ наиболее общее (то есть наименее ограничительное) условие на входные данные программы или её фрагмента, которое гарантирует, что после выполнения этого фрагмента будет выполнено заданное постусловие. Понятие является центральным в логике Хоара (аксиоматической семантике) и используется для доказательства корректности программ, автоматического синтеза кода и статического анализа.

Определение

Формально, пусть S — оператор (или последовательность операторов) программы, а Q — постусловие, то есть свойство, которое должно быть истинным после завершения S. Тогда слабейшее предусловие (weakest precondition, обозначается wp(S, Q)) — это такое предикатное условие P, что:

1. Корректность: если P истинно до выполнения S, то Q истинно после выполнения S.
2. Наибольшая общность: любое другое предусловие P', удовлетворяющее условию (1), является более сильным, то есть P' влечёт P (это означает, что P допускает большее множество начальных состояний, чем любое другое корректное предусловие).

Иными словами, wp(S, Q) описывает множество всех начальных состояний, из которых выполнение S гарантированно приводит к состоянию, удовлетворяющему Q. Если начальное состояние не удовлетворяет wp(S, Q), то либо выполнение S не завершится (в случае недетерминизма или бесконечного цикла), либо завершится в состоянии, не удовлетворяющем Q.

История

Понятие слабейшего предусловия было введено Эдсгером Дейкстрой в 1975 году в статье «Guarded Commands, Nondeterminacy and Formal Derivation of Programs» и развито в его книге «A Discipline of Programming» (1976). Дейкстра предложил исчисление предикатных трансформеров (predicate transformer semantics), где каждому оператору сопоставляется функция, преобразующая постусловие в слабейшее предусловие. Этот подход стал альтернативой классической логике Хоара, предложенной Тони Хоаром в 1969 году, и позволил формализовать доказательство корректности программ с недетерминизмом и циклами.

Формальное определение для различных конструкций

Слабейшее предусловие определяется рекурсивно для каждого типа оператора. Ниже приведены основные правила для императивного языка программирования.

Пропуск (skip)

Оператор skip не изменяет состояние программы. Слабейшее предусловие совпадает с постусловием: wp(skip, Q) = Q

Присваивание

Для оператора присваивания x := E, где x — переменная, а E — выражение, слабейшее предусловие получается заменой всех свободных вхождений x в Q на E: wp(x := E, Q) = Q[x := E] Например, для Q: (x > 0) и оператора x := x + 1: wp(x := x + 1, x > 0) = (x + 1 > 0) = (x > -1)

Последовательность

Для последовательности операторов S1; S2: wp(S1; S2, Q) = wp(S1, wp(S2, Q))

Условный оператор

Для условного оператора if B then S1 else S2: wp(if B then S1 else S2, Q) = (B → wp(S1, Q)) ∧ (¬B → wp(S2, Q)) Здесь → — логическая импликация. Если B истинно, то должно выполняться wp(S1, Q), иначе — wp(S2, Q).

Цикл с предусловием

Для цикла while B do S (с инвариантом) слабейшее предусловие определяется как наименьшая фиксированная точка (least fixed point) некоторого предикатного трансформера. В практических доказательствах используется инвариант цикла I и условие завершения (вариант). Формально: wp(while B do S, Q) = (∃ k ≥ 0) H_k(Q), где H_0(Q) = ¬B ∧ Q, а H_{k+1}(Q) = (¬B ∧ Q) ∨ (B ∧ wp(S, H_k(Q))).

Свойства

Слабейшее предусловие обладает рядом важных свойств, которые используются в доказательствах корректности:

• Закон исключённого чуда (law of the excluded miracle): wp(S, false) = false. Это означает, что никакая программа не может гарантировать ложное постусловие из любого начального состояния.
• Монотонность: если Q1 влечёт Q2, то wp(S, Q1) влечёт wp(S, Q2).
• Дистрибутивность конъюнкции: wp(S, Q1 ∧ Q2) = wp(S, Q1) ∧ wp(S, Q2).
• Дистрибутивность дизъюнкции: wp(S, Q1 ∨ Q2) = wp(S, Q1) ∨ wp(S, Q2) (для детерминированных программ).

Применение

Доказательство корректности программ

Слабейшее предусловие используется для формального доказательства того, что программа удовлетворяет своей спецификации. Для заданного постусловия Q вычисляется wp(S, Q), и затем проверяется, что фактическое предусловие (например, предусловие, заданное в спецификации) влечёт wp(S, Q). Если это так, программа корректна.

Автоматический синтез программ

Исчисление предикатных трансформеров лежит в основе некоторых методов автоматического синтеза кода: по заданному постусловию и известной структуре программы можно вычислить необходимые предусловия и, обратным ходом, построить тело программы.

Статический анализ и верификация

Современные инструменты статического анализа (например, Infer от Facebook, Frama-C, SPARK Ada) используют слабейшие предусловия для генерации условий верификации (verification conditions), которые затем передаются SMT-решателям (Z3, CVC4) для автоматической проверки.

Тестирование

Понятие слабейшего предусловия применяется в тестировании на основе моделей (model-based testing) для генерации тестовых данных: если известно wp(S, Q), то можно выбрать начальные состояния, которые гарантированно приведут к выполнению Q, что помогает создавать целенаправленные тесты.

Пример

Рассмотрим фрагмент программы на псевдокоде: `` x := x + 1; y := x * 2 ` Пусть постусловие Q: (y > 10)`. Вычислим слабейшее предусловие:

1. wp(y := x 2, y > 10) = (x 2 > 10) = (x > 5)
2. wp(x := x + 1, x > 5) = (x + 1 > 5) = (x > 4)

Таким образом, wp(S, Q) = (x > 4). Это означает, что если до выполнения программы x > 4, то после её выполнения y будет больше 10.

Связь с другими понятиями

• Сильнейшее постусловие (strongest postcondition) — двойственное понятие: это наиболее точное описание состояния после выполнения оператора, исходя из заданного предусловия. В отличие от слабейшего предусловия, которое идёт от постусловия назад, сильнейшее постусловие идёт от предусловия вперёд.
• Логика Хоара (Hoare logic) использует тройки {P} S {Q}, где P — предусловие, Q — постусловие. Слабейшее предусловие позволяет выразить тройку Хоара как P → wp(S, Q).
• Предикатный трансформер — функция, отображающая постусловие в слабейшее предусловие. Исчисление Дейкстры является одной из форм предикатных трансформеров.

Критика и ограничения

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

Источники

• Dijkstra, E. W. (1976). A Discipline of Programming. Prentice-Hall.
• Gries, D. (1981). The Science of Programming. Springer-Verlag.
• Hoare, C. A. R. (1969). "An axiomatic basis for computer programming". Communications of the ACM.
• Winskel, G. (1993). The Formal Semantics of Programming Languages. MIT Press.