Введение

Переформулирование логики Флойда — Хоара
Семантика преобразователей предикатов была введена Эдсгером Дейкстрой в его основополагающей работе «Охраняемые команды, недетерминизм и формальное выведение программ». Она определяет семантику императивной парадигмы программирования, сопоставляя каждому оператору в этом языке соответствующий преобразователь предиката: тотальную функцию между двумя предикатами на пространстве состояний оператора. В этом смысле семантика преобразователей предикатов является разновидностью денотационной семантики. Фактически, в охраняемых командах Дейкстра использует только один вид преобразователя предиката: хорошо известные слабые предусловия (см. ниже). Более того, семантика преобразователей предикатов является переформулировкой логики Флойда — Хоара. В то время как логика Хоара представлена как дедуктивная система, семантика преобразователей предикатов (либо с использованием слабых предусловий, либо с использованием сильных пост-условий, см. ниже) представляет собой полную стратегию для построения корректных дедукций логики Хоара. Иными словами, она предоставляет эффективный алгоритм для сведения задачи проверки тройки Хоара к задаче доказательства формулы первого порядка. Технически, семантика преобразователей предикатов выполняет своего рода символьное исполнение операторов в предикаты: исполнение происходит в обратном направлении в случае слабых предусловий или в прямом направлении в случае сильных пост-условий.

Определение

Для утверждения S и пост-условия R, самым слабым предварительным условием является предикат Q, такой, что для любого предварительного условия P, выполняется следующее: если и только если. Иными словами, это "наименее жесткое" или наименее ограничивающее требование, необходимое для гарантии, что R будет истинно после выполнения S. Единственность легко вытекает из определения: если и Q, и Q' являются самыми слабыми предварительными условиями, то по определению, и , а значит, . Мы часто используем wp(S, R) для обозначения самого слабого предварительного условия для утверждения S относительно пост-условия R.

Конвенции

Мы используем T для обозначения предиката, который истинен во всех случаях, и F для обозначения предиката, который ложен во всех случаях. Нам не следует, по крайней мере концептуально, смешивать это с булевым выражением, определенным синтаксисом какого-либо языка, который также может содержать значения "истина" и "ложь" как булевы скаляры. Для таких скаляров необходимо выполнить приведение типов, чтобы обеспечить соответствие T = предикат(истина) и F = предикат(ложь). Это приведение часто выполняется неявно, поэтому люди склонны воспринимать T как "истина", а F как "ложь".

Недетерминированные защищенные команды

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

Повторение

Повторение является обобщением оператора while подобным образом.

Трансформаторы предиката Win и sin

Лесли Лэмпорт предложил "win" (выигрыш) и "sin" (грех) как преобразователи предикатов для параллельного программирования.

Свойства предикатовых трансформаторов

В этом разделе представлены некоторые характерные свойства предикатных трансформаторов. Далее, S обозначает предикатный трансформатор (функцию между двумя предикатами на пространстве состояний), а P – предикат. Например, S(P) может обозначать wp(S,P) или sp(S,P). Мы будем использовать x как переменную пространства состояний.

Монотонный

Предикатные трансформаторы, представляющие интерес (wp, wlp и sp), являются монотонными. Предикатный трансформатор S является монотонным тогда и только тогда, когда:

Это свойство связано с правилом следствия в логике Хоара.

Приложения

Вычисления наиболее слабых предварительных условий широко используются для статической проверки утверждений в программах с помощью теоремы доказывания (например, SMT-решателей или систем поддержки доказательств): см. Frama C или ESC/Java2. В отличие от многих других семантических формализмов, семантика преобразования предикатов не разрабатывалась как исследование основ вычислений. Скорее, она была создана для того, чтобы предоставить программистам методологию разработки программ как "корректных по построению" в "вычислительном стиле". Этот подход "сверху вниз" пропагандировали Дейкстра и Н. Вирт. Он был дополнительно формализован Р. Дж. Бэком и другими в исчислении уточнения. Некоторые инструменты, такие как метод B, теперь обеспечивают автоматизированное рассуждение для поддержки этой методологии. В метатеории логики Хоара, наиболее слабые предварительные условия выступают как ключевое понятие в доказательстве относительной полноты.

Слабое предварительное условие и сильное последующее условие императивных выражений

В семантике предикатов-трансформаторов выражения ограничены терминами логики (см. выше). Однако это ограничение представляется излишне строгим для большинства существующих языков программирования, где выражения могут вызывать побочные эффекты (например, вызов функции с побочными эффектами), не завершаться или приводить к аварийному завершению (например, деление на ноль). Существует множество предложений по расширению концепций наименьших предварительных условий или наибольших пост-условий для императивных языков выражений и, в частности, для монад. Одной из таких разработок является теория типов Хоара, объединяющая логику Хоара для языка, подобного Хаскеллу, логику разделения и теорию типов. В настоящее время эта система реализована в виде библиотеки Coq под названием Ynot. В этом языке вычисление выражений соответствует вычислению наибольших пост-условий.