semántica de transformadores de predicados

Para una proposición S y una postcondición R , una precondición más débil es un predicado Q tal que para cualquier precondición P ,${\displaystyle \{P\}S\{R\}}$si y solo si${\displaystyle P\Rightarrow Q}$En otras palabras, es el requisito "más laxo" o menos restrictivo necesario para garantizar que R se cumpla después de S. La unicidad se deduce fácilmente de la definición: si tanto Q como Q' son precondiciones más débiles, entonces por definición${\displaystyle \{Q'\}S\{R\}}$entonces${\displaystyle Q'\Rightarrow Q}$y${\displaystyle \{Q\}S\{R\}}$entonces${\displaystyle Q\Rightarrow Q'}$y por lo tanto${\displaystyle Q=Q'}$A menudo usamos${\displaystyle wp(S,R)}$para denotar la precondición más débil para la afirmación S con respecto a una postcondición R.

Usamos T para denotar el predicado que es verdadero en todas partes y F para denotar el que es falso en todas partes. No deberíamos confundirnos, al menos conceptualmente, con una expresión booleana definida por la sintaxis de algún lenguaje, que también podría contener verdadero y falso como escalares booleanos. Para tales escalares, necesitamos realizar una conversión de tipo tal que tengamos T = predicado(verdadero) y F = predicado(falso). Esta conversión se realiza a menudo de forma informal, por lo que la gente tiende a considerar T como verdadero y F como falso.

A continuación, presentamos dos precondiciones más débiles equivalentes para la declaración de asignación. En estas fórmulas,${\displaystyle R[x\leftarrow E]}$es una copia de R donde las ocurrencias libres de x se reemplazan por E. Por lo tanto, aquí, la expresión E se convierte implícitamente en un término válido de la lógica subyacente: es, por lo tanto, una expresión pura , totalmente definida, terminante y sin efectos secundarios.

• versión 1:

• versión 2:

Siempre que E esté bien definido, aplicamos la llamada regla de un punto a la versión 1. Entonces

La primera versión evita una posible duplicación de x en R , mientras que la segunda versión es más simple cuando hay como máximo una sola aparición de x en R. La primera versión también revela una profunda dualidad entre la precondición más débil y la postcondición más fuerte (véase más abajo).

Un ejemplo de cálculo válido de wp (usando la versión 2) para asignaciones con la variable x de valor entero es:

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

Esto significa que, para que la postcondición x > 10 sea verdadera después de la asignación, la precondición x > 15 debe ser verdadera antes de la asignación. Esta es también la "precondición más débil", ya que es la restricción "más débil" sobre el valor de x que hace que x > 10 sea verdadera después de la asignación.

Por ejemplo,

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

Por ejemplo:

${\displaystyle {\begin{array}{rcl}wp({\texttt {if}}\ x<y\ {\texttt {entonces}}\ 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}}}$

En realidad, el lenguaje de comandos protegidos (GCL) de Dijkstra es una extensión del lenguaje imperativo simple presentado hasta ahora con enunciados no deterministas. De hecho, GCL pretende ser una notación formal para definir algoritmos. Los enunciados no deterministas representan opciones que quedan a la implementación real (en un lenguaje de programación efectivo): las propiedades demostradas en los enunciados no deterministas se garantizan para todas las posibles opciones de implementación. En otras palabras, las precondiciones más débiles de los enunciados no deterministas garantizan

• que existe una ejecución que termina (por ejemplo, existe una implementación),
• y que el estado final de toda ejecución que termina satisface la postcondición.

Las definiciones de precondición más débil dadas anteriormente (en particular para el bucle while ) preservan esta propiedad.

El cálculo de refinamiento extiende GCL con la noción de declaración de especificación . Sintácticamente, preferimos escribir una declaración de especificación como

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

que especifica un cálculo que comienza en un estado que satisface pre y está garantizado que terminará en un estado que satisface post cambiando solo x . Lo llamamos${\displaystyle l}$una constante lógica empleada para ayudar en una especificación. Por ejemplo, podemos especificar un cálculo que incremente x en 1 como

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

Otro ejemplo es el cálculo de la raíz cuadrada de un número entero.

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

La declaración de especificación se presenta como una instrucción primitiva en el sentido de que no contiene otras instrucciones. Sin embargo, es muy expresiva, ya que pre y post son predicados arbitrarios. Su precondición más débil es la siguiente.

Combina la idea sintáctica de Morgan con la idea de nitidez de Bijlsma, Matthews y Wiltink. ^{[ 1 ]} La principal ventaja de esto es su capacidad para definir wp de goto L y otras sentencias de salto. ^{[ 2 ]}

La formalización de sentencias de salto como goto L requiere un proceso largo y accidentado. Una creencia común parece indicar que la sentencia goto solo podría argumentarse operacionalmente. Esto probablemente se deba a la falta de reconocimiento de que goto L es en realidad milagroso (es decir, no estricto) y no sigue la Ley de Exclusión de Milagros acuñada por Dijkstra, tal como se presenta en sí misma. Pero goza de una visión operacional extremadamente simple desde la perspectiva de la precondición más débil, lo cual fue inesperado. Definimos

Para la ejecución goto L, el control se transfiere a la etiqueta L en la que debe cumplirse la precondición más débil. La forma en que se hace referencia a wpL en la regla no debería ser una gran sorpresa. Es solo ⁠${\displaystyle wp(L:S,Q)}$para alguna Q calculada hasta ese punto. Esto es como cualquier regla wp, que utiliza sentencias constituyentes para dar definiciones wp, aunque goto L parezca una primitiva. La regla no requiere la unicidad para las ubicaciones donde wpL se cumple dentro de un programa, por lo que teóricamente permite que la misma etiqueta aparezca en múltiples ubicaciones siempre que la precondición más débil en cada ubicación sea la misma wpL. La sentencia goto puede saltar a cualquiera de dichas ubicaciones. Esto justifica que podríamos colocar las mismas etiquetas en la misma ubicación varias veces, ya que${\displaystyle S(L:L:S1)}$⁠ , que es lo mismo que ⁠${\displaystyle S(L:S1)}$Además , no implica ninguna regla de ámbito, lo que permite, por ejemplo, un salto dentro del cuerpo de un bucle. Calculemos wp del siguiente programa S, que tiene un salto dentro del cuerpo del bucle.

 wp(do x > 0 → L: x := x-1 od; if x < 0 → x := -x; goto L ⫿ x ≥ 0 → skip fi, post) = { reglas de composición y alternancia secuenciales } wp(do x > 0 → L: x := x-1 od, (x<0 ∧ wp(x := -x; goto L, post)) ∨ (x ≥ 0 ∧ post) = { composición secuencial, ir a, reglas de asignación } wp(do x > 0 → L: x := x-1 od, x<0 ∧ wpL(x ← -x) ∨ x≥0 ∧ post) = { regla de repetición } la solución más fuerte de Z: [ Z ≡ x > 0 ∧ wp(L: x := x-1, Z) ∨ x < 0 ∧ wpL(x ← -x) ∨ x=0 ∧ post ] = { regla de asignación, encontrado wpL = Z(x ← x-1) } la solución más fuerte de Z: [ Z ≡ x > 0 ∧ Z(x ← x-1) ∨ x < 0 ∧ Z(x ← x-1) (x ← -x) ∨ x=0 ∧ post] = { sustitución } la solución más fuerte de Z:[ Z ≡ x > 0 ∧ Z(x ← x-1) ∨ x < 0 ∧ Z(x ← -x-1) ∨ x=0 ∧ post ] = { resolver la ecuación por aproximación } post(x ← 0)

Por lo tanto,

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

Una variante importante de la condición previa más débil es la condición previa liberal más débil.${\displaystyle wlp(S,R)}$, que produce la condición más débil bajo la cual S no termina o establece R. Por lo tanto, difiere de wp en que no garantiza la terminación. De ahí que corresponda a la lógica de Hoare en corrección parcial: para el lenguaje de sentencias dado anteriormente, wlp difiere de wp solo en el bucle while , en que no requiere una variante (ver más arriba).

Dado S una proposición y R una precondición (un predicado sobre el estado inicial), entonces ${\displaystyle sp(S,R)}$es su postcondición más fuerte : implica cualquier postcondición satisfecha por el estado final de cualquier ejecución de S, para cualquier estado inicial que satisfaga R. En otras palabras, una tripleta de Hoare${\displaystyle \{P\}S\{Q\}}$es demostrable en lógica de Hoare si y solo si se cumple el predicado siguiente:

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

Por lo general, las postcondiciones más fuertes se utilizan en la corrección parcial. Por lo tanto, tenemos la siguiente relación entre las precondiciones liberales más débiles y las postcondiciones más fuertes:

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

Por ejemplo, en la tarea tenemos:

Arriba, la variable lógica y representa el valor inicial de la variable x . Por lo tanto,

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

En la secuencia, parece que sp avanza (mientras que wp retrocede):

Leslie Lamport ha sugerido win y sin como transformadores de predicados para la programación concurrente . ^{[ 3 ]}

Los transformadores de predicados de interés ( wp , wlp y sp ) son monótonos . Un transformador de predicados S es monótono si y solo si:

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

Esta propiedad está relacionada con la regla de consecuencia de la lógica de Hoare .

Un transformador de predicados S es estricto si y solo si:

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

Por ejemplo, wp se hace artificialmente estricto, mientras que wlp generalmente no lo es. En particular, si la instrucción S no puede terminar entonces ${\displaystyle wlp(S,{\texttt {F}})}$es satisfactorio. Tenemos

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

En efecto, T es un invariante válido de ese bucle.

Los transformadores de predicados no estrictos pero monótonos o conjuntivos se denominan milagrosos y también pueden usarse para definir una clase de construcciones de programación, en particular, las sentencias de salto, que a Dijkstra le importaban menos. Estas sentencias de salto incluyen goto L directo, break y continue en un bucle y sentencias return en el cuerpo de un procedimiento, manejo de excepciones, etc. Resulta que todas las sentencias de salto son milagrosos ejecutables, ^{[ 5 ]} es decir, pueden implementarse pero no son estrictas.

Un transformador de predicados S termina si:

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

En realidad, esta terminología solo tiene sentido para los transformadores de predicados estrictos: de hecho,${\displaystyle wp(S,{\texttt {T}})}$es la condición previa más débil que garantiza la terminación de S.

Parece más apropiado denominar a esta propiedad "no abortiva" : en su corrección total, la no terminación es aborto, mientras que en su corrección parcial, no lo es.

Un transformador de predicados S es conjuntivo si y solo si:

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

Este es el caso de${\displaystyle wp(S,.)}$, incluso si la declaración S no es determinista como una declaración de selección o una declaración de especificación.

Un transformador de predicados S es disyuntivo si y solo si:

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

Este no suele ser el caso de${\displaystyle wp(S,.)}$cuando S no es determinista. De hecho, consideremos una proposición no determinista S que elige un valor booleano arbitrario. Esta proposición se presenta aquí como la siguiente proposición de selección :

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

Entonces,${\displaystyle wp(S,R)}$se reduce a la fórmula${\displaystyle R[x\leftarrow 0]\wedge R[x\leftarrow 1]}$.

Por eso,${\displaystyle wp(S,\ x=0\vee x=1)}$se reduce a la tautología${\displaystyle (0=0\vee 0=1)\wedge (1=0\vee 1=1)}$

Mientras que la fórmula${\displaystyle wp(S,x=0)\vee wp(S,x=1)}$ reduce a la proposición errónea${\displaystyle (0=0\wedge 1=0)\vee (1=0\wedge 1=1)}$.

En la semántica de transformadores de predicados, las expresiones se restringen a los términos de la lógica (véase más arriba). Sin embargo, esta restricción parece demasiado fuerte para la mayoría de los lenguajes de programación existentes, donde las expresiones pueden tener efectos secundarios (llamada a una función con efecto secundario), pueden no terminar o abortar (como la división por cero ). Existen muchas propuestas para extender las precondiciones más débiles o las postcondiciones más fuertes para lenguajes de expresiones imperativas y, en particular, para mónadas .

Entre ellas, la teoría de tipos de Hoare combina la lógica de Hoare para un lenguaje similar a Haskell , la lógica de separación y la teoría de tipos . ^{[ 9 ]} Este sistema se implementa como una biblioteca Rocq llamada Ynot . ^{[ 10 ]} En este lenguaje, la evaluación de expresiones corresponde a cálculos de postcondiciones más fuertes .

Los transformadores de predicados probabilísticos son una extensión de los transformadores de predicados para programas probabilísticos . Dichos programas tienen muchos usos en criptografía (ocultar información mediante ruido aleatorio) y computación distribuida (ruptura de simetría). ^{[ 11 ]}