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

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

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

Слабые предварительные условия [ править ]

Определение [ править ]

Для заявления S и постусловия R , слабое предварительное условие является предикат Q такое , что для любого предусловия , если и только если . Другими слова, это «самое общие » или наименее ограничительное требование , необходимое для гарантии того, что R имеет место после того, как S . Уникальность легко следует из определения: Если оба Q и Q» являются слабыми предпосылками, то по определению , так и так , и , таким образом . Обозначим через слабейшее предусловие для утверждения S и постусловие R${\ displaystyle P}$${\ 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)}$.

Пропустить [ править ]

${\ displaystyle wp ({\ textbf {skip}}, R) \ = \ R}$

Прервать [ править ]

${\ displaystyle wp ({\ textbf {abort}}, R) \ = \ {\ textbf {false}}}$

Назначение [ править ]

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

• версия 1:

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

• версия 2:

${\ Displaystyle WP (х: = E, R) \ = \ R [х \ leftarrow E]}$

Первая версия избегает потенциального дублирования E в 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 wp(S_{1};S_{2},R)\ =\ wp(S_{1},wp(S_{2},R))}$

Например,

${\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 wp({\textbf {if}}\ E\ {\textbf {then}}\ S_{1}\ {\textbf {else}}\ S_{2}\ {\textbf {end}},R)\ =\ (E\Rightarrow wp(S_{1},R))\wedge (\neg E\Rightarrow wp(S_{2},R))}$

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

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

Пока цикл [ править ]

Частичная корректность [ править ]

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

${\displaystyle wlp({\textbf {while}}\ E\ {\textbf {do}}\ S\ {\textbf {done}},R)\ =\ {\begin{array}{l}I\\\wedge \ \forall y,((E\wedge I)\Rightarrow wlp(S,I))[x\leftarrow y]\\\wedge \ \forall y,((\neg E\wedge I)\Rightarrow R)[x\leftarrow y]\end{array}}}$

Это просто утверждает, что (1) инвариант должен сохраняться в начале цикла; (2) дополнительно, для любого начального состояния y инвариант и защита, вместе взятые, должны быть достаточно сильными, чтобы установить самое слабое предварительное условие, необходимое для того, чтобы тело цикла могло восстановить инвариант; (3) наконец, если и когда цикл завершается в заданном состоянии y , тот факт, что защита цикла ложна вместе с инвариантом, должен иметь возможность установить требуемое постусловие.

Полная правильность [ править ]

Чтобы показать полную корректность, мы также должны показать, что цикл завершается. Для этого мы определяем хорошо обоснованное отношение в пространстве состояний, обозначенное «<» и называемое вариантом цикла . Следовательно, мы имеем:

${\displaystyle wp({\textbf {while}}\ E\ {\textbf {do}}\ S\ {\textbf {done}},R)\ =\ {\begin{array}{l}I\\\wedge \ \forall y,((E\wedge I)\Rightarrow wp(S,I\wedge x<y))[x\leftarrow y]\\\wedge \ \forall y,((\neg E\wedge I)\Rightarrow R)[x\leftarrow y]\end{array}}}$ где y - свежий набор переменных

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

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

В семантике преобразователей предикатов инвариант и вариант строятся путем имитации теоремы Клини о неподвижной точке . Ниже эта конструкция описана в теории множеств . Мы предполагаем, что U - это множество, обозначающее пространство состояний. Сначала мы определяем семейство подмножеств U, обозначаемых индукцией по натуральному числу k . Неформально представляет набор начальных состояний, которые удовлетворяют R после менее чем k итераций цикла: ${\displaystyle (A_{k})_{k\in \mathbb {N} }}$ ${\displaystyle A_{k}}$

${\displaystyle {\begin{array}{rcl}A_{0}&=&\emptyset \\A_{k+1}&=&\left\{\ y\in U\ |\ ((E\Rightarrow wp(S,x\in A_{k}))\wedge (\neg E\Rightarrow R))[x\leftarrow y]\ \right\}\\\end{array}}}$

Затем мы определяем:

• инвариант I как предикат .${\displaystyle \exists k,x\in A_{k}}$
• вариант как предложение${\displaystyle y<z}$${\displaystyle \exists i,y\in A_{i}\wedge (\forall j,z\in A_{j}\Rightarrow i<j)}$

С этими определениями сводится к формуле .${\displaystyle wp({\textbf {while}}\ E\ {\textbf {do}}\ S\ {\textbf {done}},R)}$${\displaystyle \exists k,x\in A_{k}}$

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

Недетерминированные охраняемые команды [ править ]

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

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

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

Выбор [ править ]

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

${\displaystyle wp(\mathbf {if} \ E_{1}\rightarrow S_{1}\ [\!]\ \ldots \ [\!]\ E_{n}\rightarrow S_{n}\ \mathbf {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}}}$

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

Повторение [ править ]

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

Заявление спецификации (или самое слабое предварительное условие вызова процедуры) [ править ]

Исчисление уточнений расширяет недетерминированные утверждения понятием оператора спецификации . Неформально этот оператор представляет собой вызов процедуры в черном ящике, где тело процедуры неизвестно. Как правило, с использованием синтаксиса близко к B-метода , A спецификация заявление написано

${\displaystyle P\ |}$ @${\displaystyle y.\ Q\rightarrow x:=y}$

куда

• x - глобальная переменная, измененная оператором,
• P - предикат, представляющий предусловие,
• y - это новая логическая переменная, связанная в Q , которая представляет новое значение x, недетерминированно выбранное оператором,
• Q - это предикат, представляющий постусловие, или, точнее, охранник: в Q переменная x представляет начальное состояние, а y обозначает конечное состояние.

Самым слабым предварительным условием утверждения спецификации является:

${\displaystyle wp(P\ |}$ @${\displaystyle y.\ Q\rightarrow x:=y\ ,\ R)\ =\ P\wedge \forall z,Q[y\leftarrow z]\Rightarrow R[x\leftarrow z]}$ где z - новое имя

Более того, оператор S реализует такой оператор спецификации тогда и только тогда, когда следующий предикат является тавтологией:

${\displaystyle \forall x_{0},(P\Rightarrow wp(S,Q[x\leftarrow x_{0}][y\leftarrow x]))[x\leftarrow x_{0}]}$ где - новое имя (обозначающее начальное состояние)${\displaystyle x_{0}}$

Действительно, в таком случае для всех постусловий R обеспечивается следующее свойство (это прямое следствие монотонности wp , см. Ниже):

${\displaystyle wp(P\ |}$ @${\displaystyle y.\ Q\rightarrow x:=y\ ,\ R)\Rightarrow wp(S,R)}$

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

Другие преобразователи предикатов [ править ]

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

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

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

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

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

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

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

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

Преобразователи предикатов Win и Sin [ править ]

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

Свойства предикатных преобразователей [ править ]

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

Монотонный [ править ]

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

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

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

Строгий [ править ]

Преобразователь предикатов T является строгим тогда и только тогда:

${\displaystyle T(\mathbf {false} )\ \Leftrightarrow \ \mathbf {false} }$

Например, wp является строгим, а wlp - нет. В частности, если оператор S не может завершиться, то он выполним. У нас есть${\displaystyle wlp(S,\mathbf {false} )}$

${\displaystyle wlp(\mathbf {while} \ \mathbf {true} \ \mathbf {do} \ \mathbf {skip} \ \mathbf {done} ,\mathbf {false} )\ \Leftrightarrow \mathbf {true} }$

В самом деле, true - допустимый инвариант этого цикла.

Завершение [ править ]

Предикат трансформатор Т есть оконечный тогда и только тогда:

${\displaystyle T(\mathbf {true} )\ \Leftrightarrow \ \mathbf {true} }$

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

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

Конъюнктив [ править ]

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

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

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

Дизъюнктивный [ править ]

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

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

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

${\displaystyle S\ =\ \mathbf {if} \ \mathbf {true} \rightarrow x:=0\ [\!]\ \mathbf {true} \rightarrow x:=1\ \mathbf {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)}$

Тот же контрпример можно воспроизвести, используя вместо этого оператор спецификации (см. Выше):

${\displaystyle S\ =\ \mathbf {true} \ |}$ @${\displaystyle y.\ y\in \{0,1\}\rightarrow x:=y}$

Приложения [ править ]

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

Помимо преобразователей предикатов [ править ]

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

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

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

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

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

См. Также [ править ]

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

Заметки [ править ]

Ссылки [ править ]