Семантика предикатного трансформатора

Переформулировка логики Флойда-Хора

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

Более того, семантика предикатного трансформатора является переформулировкой логики Флойда–Хоара . В то время как логика Хоара представлена ​​как дедуктивная система , семантика предикатного трансформатора (либо по слабейшим предусловиям , либо по сильнейшим постусловиям , см. ниже) является полной стратегией построения допустимых выводов логики Хоара. Другими словами, они предоставляют эффективный алгоритм для сведения проблемы проверки тройки Хоара к проблеме доказательства формулы первого порядка . Технически, семантика предикатного трансформатора выполняет своего рода символическое исполнение утверждений в предикаты: исполнение выполняется назад в случае слабейших предусловий или вперед в случае сильнейших постусловий.

Самые слабые предпосылки

Определение

Для утверждения S и постусловия R слабейшее предусловие — это предикат Q такой, что для любого предусловия P , тогда и только тогда . Другими словами, это «самое свободное» или наименее ограничительное требование, необходимое для гарантии того, что R выполняется после S . Уникальность легко следует из определения: если и Q, и Q' являются слабейшими предусловиями, то по определению так и так , и таким образом . Мы часто используем для обозначения слабейшего предусловия для утверждения S относительно постусловия R . ${\displaystyle \{P\}S\{R\}}$ ${\displaystyle P\Rightarrow Q}$ ${\displaystyle \{Q'\}S\{R\}}$ ${\displaystyle Q'\Rightarrow Q}$ ${\displaystyle \{Q\}S\{R\}}$ ${\displaystyle Q\Rightarrow Q'}$ ${\displaystyle Q=Q'}$ ${\displaystyle wp(S,R)}$

Конвенции

Мы используем T для обозначения предиката, который везде истинен, и F для обозначения предиката, который везде ложен. Мы не должны, по крайней мере, концептуально путать себя с булевым выражением, определенным некоторым синтаксисом языка, который также может содержать true и false как булевы скаляры. Для таких скаляров нам нужно выполнить приведение типа, так что у нас будет T = predicate(true) и F = predicate(false). Такое продвижение часто выполняется небрежно, поэтому люди склонны считать T истинным, а F — ложным.

Пропускать

Прервать

Назначение

Ниже мы приводим два эквивалентных слабейших предварительных условия для оператора присваивания. В этих формулах есть копия R , где свободные вхождения x заменяются на E. Следовательно, здесь выражение E неявно приводится к допустимому термину базовой логики: таким образом, это чистое выражение, полностью определенное, завершающееся и без побочных эффектов. ${\displaystyle R[x\leftarrow E]}$

• версия 1:

• версия 2:

При условии, что E хорошо определено, мы просто применяем так называемое правило одной точки к версии 1. Тогда

Первая версия позволяет избежать потенциального дублирования x в R , тогда как вторая версия проще, когда x встречается не более одного раза в R. Первая версия также раскрывает глубокую двойственность между слабейшим предусловием и сильнейшим постусловием (см. ниже).

Пример допустимого расчета wp (с использованием версии 2) для присваиваний с целочисленной переменной x :

${\displaystyle {\begin{array}{rcl}wp(x:=x-5,x>10)&=&x-5>10\\&\Leftrightarrow &x>15\end{array}}}$

Это означает, что для того, чтобы постусловие x > 10 было истинным после присваивания, предусловие x > 15 должно быть истинным до присваивания. Это также «слабейшее предусловие», поскольку это «слабейшее» ограничение на значение x , которое делает x > 10 истинным после присваивания.

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

Например,

${\displaystyle {\begin{array}{rcl}wp(x:=x-5;x:=x*2\ ,\ x>20)&=&wp(x:=x-5,wp(x:=x*2,x>20))\\&=&wp(x:=x-5,x*2>20)\\&=&(x-5)*2>20\\&=&x>15\end{array}}}$

Условный

Например:

${\displaystyle {\begin{array}{rcl}wp({\texttt {if}}\ x<y\ {\texttt {then}}\ x:=y\ {\texttt {else}}\;\;{\texttt {skip}}\;\;{\texttt {end}},\ x\geq y)&=&(x<y\Rightarrow wp(x:=y,x\geq y))\ \wedge \ (\neg (x<y)\Rightarrow wp({\texttt {skip}},x\geq y))\\&=&(x<y\Rightarrow y\geq y)\ \wedge \ (\neg (x<y)\Rightarrow x\geq y)\\&\Leftrightarrow &{\texttt {true}}\end{array}}}$

Цикл While

Частичная правильность

Оставив на мгновение вопрос о завершении, мы можем определить правило для самого слабого либерального предварительного условия , обозначаемого wlp , используя предикат INV , называемый Loop INV ariant , который обычно предоставляется программистом:

Полная корректность

Чтобы показать полную корректность, мы также должны показать, что цикл завершается. Для этого мы определяем обоснованное отношение на пространстве состояний, обозначенное как ( wfs , <) и определяем вариантную функцию vf , так что мы имеем:

Неформально, в приведенном выше соединении трех формул:

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

Однако, соединение этих трех не является необходимым условием. Точно, у нас есть

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

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

• что существует завершающее выполнение (например, существует реализация),
• и что конечное состояние всех завершающихся выполнений удовлетворяет постусловию.

Обратите внимание, что определения слабейшего предусловия, данные выше (в частности, для цикла while ), сохраняют это свойство.

Выбор

Выборка представляет собой обобщение оператора if :

^{[ необходима ссылка ]}

Здесь, когда два охранника и одновременно истинны, то выполнение этого оператора может запустить любой из связанных операторов или . ${\displaystyle E_{i}}$ ${\displaystyle E_{j}}$ ${\displaystyle S_{i}}$ ${\displaystyle S_{j}}$

Повторение

Повторение — это обобщение оператора while аналогичным образом.

Заявление о спецификации

Исчисление уточнения расширяет GCL с помощью понятия утверждения спецификации . Синтаксически мы предпочитаем записывать утверждение спецификации как

  ${\displaystyle x:l[pre,post]}$

который определяет вычисление, которое начинается в состоянии, удовлетворяющем pre , и гарантированно заканчивается в состоянии, удовлетворяющем post, изменяя только x . Мы называем логическую константу, используемую для помощи в спецификации. Например, мы можем определить вычисление, которое увеличивает x на 1 как ${\displaystyle l}$

  ${\displaystyle x:l[x=l,x=l+1]}$

Другим примером является вычисление квадратного корня целого числа.

  ${\displaystyle x:l[x=l^{2},x=l]}$

Утверждение спецификации выглядит как примитив в том смысле, что оно не содержит других утверждений. Однако оно очень выразительно, поскольку pre и post являются произвольными предикатами. Его самое слабое предварительное условие следующее.

Он сочетает в себе синтаксическую идею Моргана с идеей резкости Бийлсмы, Мэтьюза и Уилтинка. ^[1] Главное преимущество этого — возможность определения wp для goto L и других операторов перехода. ^[2]

Перейти к заявлению

Формализация операторов перехода, таких как goto L, занимает очень долгий и ухабистый процесс. Распространенное мнение, похоже, указывает на то, что оператор goto может быть аргументирован только операционально. Вероятно, это связано с неспособностью распознать, что goto L на самом деле является чудом (т. е. нестрогим) и не следует придуманному Дейкстрой Закону Исключенного Чуда, как он есть сам по себе. Но он имеет чрезвычайно простой операциональный вид с точки зрения самого слабого предварительного условия, что было неожиданно. Мы определяем

Для goto L выполнение передает управление метке L , в которой должно выполняться самое слабое предварительное условие. То, как wpL упоминается в правиле, не следует воспринимать как большой сюрприз. Это просто ⁠ ⁠ для некоторого Q, вычисленного к этой точке. Это похоже на любые правила wp, использующие составляющие операторы для задания определений wp, хотя goto L кажется примитивом. Правило не требует уникальности для мест, где wpL выполняется в программе, поэтому теоретически оно позволяет одной и той же метке появляться в нескольких местах, пока самое слабое предварительное условие в каждом месте является тем же wpL. Оператор goto может перейти в любое из таких мест. Это фактически оправдывает то, что мы могли бы размещать одни и те же метки в одном и том же месте несколько раз, как ⁠ ⁠ , что то же самое, что и ⁠ ⁠ . Кроме того, это не подразумевает никаких правил области действия, таким образом, позволяя, например, перейти в тело цикла. Рассчитаем wp следующей программы S, в которой есть переход в тело цикла. ${\displaystyle wp(L:S,Q)}$ ${\displaystyle S(L:L:S1)}$ ${\displaystyle S(L:S1)}$

 wp(do x > 0 → L: x := x-1 od; if x < 0 → x := -x; goto L ⫿ x ≥ 0 → skip fi, post) = {правила последовательного состава и чередования} wp(сделать x > 0 → L: x := x-1 od, (x<0 ∧ wp(x := -x; перейти к L, post)) ∨ (x ≥ 0 ∧ post) = {последовательная композиция, goto, правила назначения} wp(сделать x > 0 → L: x := x-1 od, x<0 ∧ wpL(x ← -x) ∨ x≥0 ∧ post) = {правило повторения} самое сильное решение Z: [ Z ≡ x > 0 ∧ wp(L: x := x-1, Z) ∨ x < 0 ∧ wpL(x ← -x) ∨ x=0 ∧ post ]  = { правило присваивания, найдено wpL = Z(x ← x-1) } самое сильное решение Z: [ Z ≡ x > 0 ∧ Z(x ← x-1) ∨ x < 0 ∧ Z(x ← x-1) (x ← -x) ∨ x=0 ∧ пост] = {подстановка} самое сильное решение Z:[ Z ≡ x > 0 ∧ Z(x ← x-1) ∨ x < 0 ∧ Z(x ← -x-1) ∨ x=0 ∧ пост ] = {решить уравнение приближенным методом} пост(x ← 0)

Поэтому,

wp(S, пост) = пост(x ← 0).

Другие предикатные трансформаторы

Самая слабая либеральная предпосылка

Важным вариантом самого слабого предусловия является самое слабое либеральное предусловие , которое дает самое слабое условие, при котором S либо не завершается, либо устанавливает R. Поэтому оно отличается от wp тем, что не гарантирует завершения. Следовательно, оно соответствует логике Хоара в частичной корректности: для языка утверждений, данного выше, wlp отличается от wp только в while-loop , не требуя варианта (см. выше). ${\displaystyle wlp(S,R)}$

Сильнейшее постусловие

Если S — утверждение, а R — предусловие ( предикат начального состояния), то — их сильнейшее постусловие : оно подразумевает любое постусловие, которому удовлетворяет конечное состояние любого выполнения S, для любого начального состояния, удовлетворяющего R. Другими словами, тройка Хоара доказуема в логике Хоара тогда и только тогда, когда выполняется следующий предикат: ${\displaystyle sp(S,R)}$ ${\displaystyle \{P\}S\{Q\}}$

${\displaystyle \forall x,sp(S,P)\Rightarrow Q}$

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

${\displaystyle (\forall x,P\Rightarrow wlp(S,Q))\ \Leftrightarrow \ (\forall x,sp(S,P)\Rightarrow Q)}$

Например, по заданию у нас есть:

Выше логическая переменная y представляет собой начальное значение переменной x . Следовательно,

${\displaystyle sp(x:=x-5,x>15)\ =\ \exists y,x=y-5\wedge y>15\ \Leftrightarrow \ x>10}$

В последовательности видно, что sp работает вперед (тогда как wp работает назад):

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

Лесли Лэмпорт предложил win и sin в качестве предикатных трансформаторов для параллельного программирования . ^[3]

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

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

Монотонный

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

${\displaystyle (\forall x:P:Q)\Rightarrow (\forall x:S(P):S(Q))}$

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

Строгий

Предикатный трансформатор S является строгим тогда и только тогда:

${\displaystyle S({\texttt {F}})\ \Leftrightarrow \ {\texttt {F}}}$

Например, wp искусственно сделан строгим, тогда как wlp, как правило, нет. В частности, если утверждение S не может быть завершено, то является выполнимым. Мы имеем ${\displaystyle wlp(S,{\texttt {F}})}$

${\displaystyle wlp({\texttt {while}}\ {\texttt {true}}\ {\texttt {do}}\ {\texttt {skip}}\ {\texttt {done}},{\texttt {F}})\ \Leftrightarrow {\texttt {T}}}$

Действительно, T является допустимым инвариантом этого цикла.

Нестрогие, но монотонные или конъюнктивные предикатные трансформаторы называются чудесными и также могут использоваться для определения класса программных конструкций, в частности, операторов перехода, которые Дейкстру волновали меньше всего. Эти операторы перехода включают прямой goto L, break и continue в цикле и операторы return в теле процедуры, обработку исключений и т. д. Оказывается, что все операторы перехода являются исполняемыми чудесами, ^{[5] т. е.} они могут быть реализованы, но не строгими.

Прекращение

Предикатный трансформатор S завершается , если:

${\displaystyle S({\texttt {T}})\ \Leftrightarrow \ {\texttt {T}}}$

На самом деле эта терминология имеет смысл только для строгих предикатных трансформаторов: действительно, является слабейшим предусловием, гарантирующим завершение S. ${\displaystyle wp(S,{\texttt {T}})}$

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

Соединительный

Предикатный трансформатор S является конъюнктивным тогда и только тогда:

${\displaystyle S(P\wedge Q)\ \Leftrightarrow \ S(P)\wedge S(Q)}$

Это имеет место , даже если оператор S недетерминирован как оператор выбора или оператор спецификации. ${\displaystyle wp(S,.)}$

Дизъюнктивный

Предикатный трансформатор S является дизъюнктивным тогда и только тогда:

${\displaystyle S(P\vee Q)\ \Leftrightarrow \ S(P)\vee S(Q)}$

Это, как правило, не тот случай, когда S недетерминирован. Действительно, рассмотрим недетерминированное утверждение S, выбирающее произвольное логическое значение. Это утверждение дано здесь как следующее утверждение выбора : ${\displaystyle wp(S,.)}$

${\displaystyle S\ =\ {\texttt {if}}\ {\texttt {true}}\rightarrow x:=0\ [\!]\ {\texttt {true}}\rightarrow x:=1\ {\texttt {fi}}}$

Тогда сводится к формуле . ${\displaystyle wp(S,R)}$ ${\displaystyle R[x\leftarrow 0]\wedge R[x\leftarrow 1]}$

Следовательно, сводится к тавтологии ${\displaystyle wp(S,\ x=0\vee x=1)}$ ${\displaystyle (0=0\vee 0=1)\wedge (1=0\vee 1=1)}$

Между тем, формула сводится к неверному предложению . ${\displaystyle wp(S,x=0)\vee wp(S,x=1)}$ ${\displaystyle (0=0\wedge 1=0)\vee (1=0\wedge 1=1)}$

Приложения

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

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

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

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

Среди них теория типов Хоара объединяет логику Хоара для языка, подобного Haskell , логику разделения и теорию типов . ^[9] В настоящее время эта система реализована в виде библиотеки Coq под названием Ynot . ^[10] В этом языке оценка выражений соответствует вычислениям сильнейших постусловий .

Вероятностные предикатные преобразователи

Вероятностные предикатные преобразователи являются расширением предикатных преобразователей для вероятностных программ . Действительно, такие программы имеют множество применений в криптографии (сокрытие информации с использованием некоторого рандомизированного шума), распределенных системах (нарушение симметрии). ^[11]

Смотрите также

• Аксиоматическая семантика — включает семантику предикатного трансформатора
• Динамическая логика — где предикатные трансформаторы появляются как модальности
• Формальная семантика языков программирования — обзор

Примечания

1. Чен, Вэй и Уддинг, Ян Теймен, «Уточненное описание спецификации» WUCS-89-37 (1989). https://openscholarship.wustl.edu/cse_research/749
2. Чэнь, Вэй, «Характеристика операторов перехода методом A wp», Международный симпозиум по теоретическим аспектам программной инженерии (TASE) 2021 г., 2021 г., стр. 15–22. doi: 10.1109/TASE52547.2021.00019.
3. Лампорт, Лесли (июль 1990 г.). «win and sin: Predicate Transformers for Concurrency». ACM Trans. Program. Lang. Syst. 12 (3): 396–428. CiteSeerX  10.1.1.33.90 . doi :10.1145/78969.78970. S2CID  209901.
4. Back, Ralph-Johan; Wright, Joakim (2012) [1978]. Refinement Calculus: A Systematic Introduction. Тексты по информатике. Springer. ISBN 978-1-4612-1674-2.
5. Чэнь, Вэй, «Заявления о выходе — это исполняемые чудеса» WUCS-91-53 (1991). https://openscholarship.wustl.edu/cse_research/671
6. Дейкстра, Эдсгер В. (1968). «Конструктивный подход к проблеме корректности программ». BIT Numerical Mathematics . 8 (3): 174–186. doi :10.1007/bf01933419. S2CID  62224342.
7. Вирт, Н. (апрель 1971 г.). «Разработка программ путем пошагового уточнения» (PDF) . Comm. ACM . 14 (4): 221–7. doi :10.1145/362575.362577. hdl : 20.500.11850/80846 . S2CID  13214445.
8. Учебник по логике Хоара: библиотека Coq , дающая простое, но формальное доказательство того, что логика Хоара является корректной и полной с точки зрения операционной семантики .
9. Наневски, Александр; Моррисетт, Грег; Биркедал, Ларс (сентябрь 2008 г.). «Теория типов Хоара, полиморфизм и разделение» (PDF) . Журнал функционального программирования . 18 (5–6): 865–911. doi :10.1017/S0956796808006953. S2CID  6956622.
10. Yне является библиотекой Coq , реализующей теорию типов Хоара.
11. Морган, Кэрролл; МакИвер, Аннабель ; Зайдель, Карен (май 1996 г.). «Вероятностные предикатные трансформаторы» (PDF) . ACM Trans. Program. Lang. Syst . 18 (3): 325–353. CiteSeerX 10.1.1.41.9219 . doi :10.1145/229542.229547. S2CID  5812195. 

Ссылки

• де Баккер, Дж. В. (1980). Математическая теория корректности программ . Prentice-Hall. ISBN 978-0-13-562132-5.
• Bonsangue, Marcello M.; Kok, Joost N. (ноябрь 1994 г.). «Самое слабое исчисление предусловий: рекурсия и двойственность». Formal Aspects of Computing . 6 (6): 788–800. CiteSeerX  10.1.1.27.8491 . doi :10.1007/BF01213603. S2CID  40323488.
• Дейкстра, Эдсгер В. (август 1975 г.). «Охраняемые команды, неопределенность и формальный вывод программ». Comm. ACM . 18 (8): 453–7. doi : 10.1145/360933.360975 . S2CID  1679242.
• Дейкстра, Эдсгер В. (1976). Дисциплина программирования . Prentice Hall. ISBN 978-0-613-92411-5.— Систематическое введение в версию защищенного командного языка с большим количеством рабочих примеров
• Дейкстра, Эдсгер В.; Схолтен, Карел С. (1990). Исчисление предикатов и семантика программ. Тексты и монографии по информатике. Спрингер-Верлаг. ISBN 978-0-387-96957-2.— Более абстрактная, формальная и определенная трактовка
• Грис, Дэвид (1981). Наука программирования . Спрингер-Верлаг. ISBN 978-0-387-96480-5.