Семантика преобразователя предикатов

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

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

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

Определение

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

Соглашения

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

Пропустить

$wp({\texttt {skip}},R)\ =\ R$

Прервать

$wp({\texttt {abort}},R)\ =\ {\texttt {F}}$

Назначение

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

• версия 1:

$wp(x:=E,R)\ =\ (\forall y.y=E\Rightarrow R[x\leftarrow y])$ где y — новая переменная, несвободная в E и R (представляющая окончательное значение переменной x )

• версия 2:

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

$wp(x:=E,R)\ =\ R[x\leftarrow E]$

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

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

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

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

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

$wp(S_{1};S_{2},R)\ =\ wp(S_{1},wp(S_{2},R))$

Например,

${\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}}$

Условно

$wp({\texttt {if}}\ E\ {\texttt {then}}\ S_{1}\ {\texttt {else}}\ S_{2}\ {\texttt {end}},R)\ =\ (E\Rightarrow wp(S_{1},R))\wedge (\neg E\Rightarrow wp(S_{2},R))$

В качестве примера:

${\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}}$

Пока цикл

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

На мгновение игнорируя завершение, мы можем определить правило для самого слабого либерального предварительного условия , обозначаемого wlp , используя предикат \textit{INV} , называемый [[loop \textit{INV}ariant]], обычно предоставляемый программистом:

$wlp({\texttt {while}}\ E\ {\texttt {do}}\ S\ {\texttt {done}},R)\Leftarrow \ {\textit {INV}}\ \ {\text{if}}\ \ {\begin{array}{l}\\(E\wedge {\textit {INV}}\Rightarrow wlp(S,{\textit {INV}}))\\\wedge \ (\neg E\wedge {\textit {INV}}\Rightarrow R)\end{array}}$

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

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

$wp({\texttt {while}}\ E\ {\texttt {do}}\ S\ {\texttt {done}},R)\ \Leftarrow \ {\textit {INV}}\ \ {\text{if}}\ \ \ \ {\begin{array}{l}\\(E\wedge {\textit {INV}}\Rightarrow {\textit {vf}}\in {\textit {wfs}})\\\wedge \ (E\wedge {\textit {INV}}\wedge v={\textit {vf}}\Rightarrow wp(S,{\textit {INV}}\wedge v<{\textit {vf}}))\\\wedge \ (\neg E\wedge {\textit {INV}}\Rightarrow R)\end{array}}$ где v — новый набор переменных

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

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

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

$wp({\texttt {while}}\ E\ {\texttt {do}}\ S\ {\texttt {done}},R)\ \ =\ \ {\text{the strongest solution of the recursive equation}}\ {\begin{array}{l}Z:[Z\equiv (E\wedge wp(S,Z))\vee (\neg E\wedge R)]\end{array}}$

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

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

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

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

Выбор

Выбор — это обобщение оператора if :

$wp({\texttt {if}}\ E_{1}\rightarrow S_{1}\ [\!]\ \ldots \ [\!]\ E_{n}\rightarrow S_{n}\ {\texttt {fi}},R)\ ={\begin{array}{l}(E_{1}\vee \ldots \vee E_{n})\\\wedge \ (E_{1}\Rightarrow wp(S_{1},R))\\\ldots \\\wedge \ (E_{n}\Rightarrow wp(S_{n},R))\\\end{array}}$

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

Повторение

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

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

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

     $x:l[pre,post]$

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

     $x:l[x=l,x=l+1]$

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

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

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

$wp(x:l[pre,post],R)=(\exists l::pre)\wedge (\forall s:(\forall l:pre:post(x\leftarrow s)):R(x\leftarrow s))$ где s свежий.

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

Оператор Goto

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

$wp({\texttt {goto}}\ L,R)=wpL$ где wpL — самое слабое предварительное условие на L. метке

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

     wp(do x > 0 → L: x := x-1 od;  if x < 0 → x := -x; goto L ⫿ x ≥ 0 → skip fi,  post)
   =   { sequential composition and alternation rules }
     wp(do x > 0 → L: x := x-1 od, (x<0 ∧ wp(x := -x; goto L, post)) ∨ (x ≥  0 ∧ post)
   =   { sequential composition, goto, assignment rules }
     wp(do x > 0 → L: x := x-1 od, x<0 ∧ wpL(x ← -x) ∨ x≥0 ∧ post)
   =   { repetition rule }
     the strongest solution of 
              Z: [ Z ≡ x > 0 ∧ wp(L: x := x-1, Z) ∨ x < 0 ∧ wpL(x ← -x) ∨ x=0 ∧ post ]    
   =  { assignment rule, found wpL = Z(x ← x-1) }
     the strongest solution of 
              Z: [ Z ≡ x > 0 ∧ Z(x ← x-1) ∨ x < 0 ∧ Z(x ← x-1) (x ← -x) ∨ x=0 ∧ post]
   =  { substitution }
     the strongest solution of 
              Z:[ Z ≡ x > 0 ∧ Z(x ← x-1) ∨ x < 0 ∧ Z(x ← -x-1) ∨ x=0 ∧ post ]
   =  { solve the equation by approximation }
     post(x ← 0)

Поэтому,

wp(S, post) = post(x ← 0).

Другие

Слабейшее

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

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

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

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

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

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

Например, по заданию имеем:

$sp(x:=E,R)\ =\ \exists y,x=E[x\leftarrow y]\wedge R[x\leftarrow y]$ где ты свежий

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

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

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

$sp(S_{1};S_{2}\ ,\ R)\ =\ sp(S_{2},sp(S_{1},R))$

Преобразователи предикатов выигрыша и греха

Лесли Лэмпорт предложил выигрыш и грех в качестве преобразователей предикатов для параллельного программирования .

Свойства преобразователей предикатов

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

Монотонный

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

$(\forall x:P:Q)\Rightarrow (\forall x:S(P):S(Q))$

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

Строгий

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

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

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

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

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

Нестрогие, но монотонные или конъюнктивные преобразователи предикатов называются чудесными и могут также использоваться для определения класса программных конструкций, в частности, операторов перехода, которые Дейкстра меньше всего заботил. Эти операторы перехода включают в себя прямой переход к L, операторы прерывания и продолжения в цикле и операторы возврата в теле процедуры, обработку исключений и т. д. Оказывается, все операторы перехода — это исполняемые чудеса, т.е. они могут быть реализованы, но не строго.

Прекращение

Преобразователь предикатов S завершается , если:

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

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

Кажется, правильнее было бы назвать это свойство непрерыванием : в полной корректности непрерывание есть аборт, а в частичной корректности - нет.

Союз

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

$S(P\wedge Q)\ \Leftrightarrow \ S(P)\wedge S(Q)$

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

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

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

$S(P\vee Q)\ \Leftrightarrow \ S(P)\vee S(Q)$

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

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

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

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

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

Приложения

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

преобразователей

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

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

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

предикатов

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

См. также

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

Ссылки

• де Баккер, JW (1980). Математическая теория корректности программ . Прентис-Холл. ISBN  978-0-13-562132-5 .
• Бонсанге, Марчелло М.; Кок, Йост Н. (ноябрь 1994 г.). «Самое слабое исчисление предусловий: рекурсия и двойственность». Формальные аспекты вычислений . 6 (6): 788–800. CiteSeerX   10.1.1.27.8491 . дои : 10.1007/BF01213603 . S2CID   40323488 .
• Дейкстра, Эдсгер В. (август 1975 г.). «Защищенные команды, неопределенность и формальный вывод программ» . Комм. АКМ . 18 (8): 453–7. дои : 10.1145/360933.360975 . S2CID   1679242 .
• Дейкстра, Эдсгер В. (1976). Дисциплина программирования . Прентис Холл. ISBN  978-0-613-92411-5 . — Систематическое введение в версию защищенного командного языка со множеством проработанных примеров.
• Дейкстра, Эдсгер В.; Схолтен, Карел С. (1990). Исчисление предикатов и семантика программ . Тексты и монографии по информатике. Спрингер-Верлаг. ISBN  978-0-387-96957-2 . — Более абстрактная, формальная и определенная трактовка
• Грис, Дэвид (1981). Наука программирования . Спрингер Верлаг. ISBN  978-0-387-96480-5 .