Axioma de asignación de Hoare

Definición

Regla que obtiene la precondición de V := E sustituyendo en la postcondición $Q$ todas las apariciones libres de $V$ por la expresión $E$.

Intuición

Después de la asignación, V contiene el valor de E calculado en el estado anterior. Para saber qué debía cumplirse antes, se reemplaza el valor final exigido para V por la expresión que lo producirá.

Formulación

$$\boxed{\{Q_E^V\}V:=E\{Q\}}.$$

La convención usada en las notas de Programación Avanzada es

$$Q_E^V\equiv Q[E/V],$$

que se lee “$Q$ con $V$ sustituida por $E$”. Así, la precondición calculada es $P=Q_E^V$. La sustitución debe ser simultánea y evitar la captura de variables.

Las diapositivas representan intuitivamente la sustitución con el esquema $\{V=E,Q\}$: se usa $V=E$ para reemplazar $V$ dentro de $Q$; no se trata de afirmar la conjunción $V=E\wedge Q$ antes de ejecutar la asignación.

Ejemplo mínimo

Q: k = 12
instrucción: k := 4*a
Q^k_{4a}: 4*a = 12
precondición simplificada: a = 3

Por tanto:

$$\{a=3\}k:=4a\{k=12\}.$$

Otro ejemplo:

$$\{i<3\}i:=2i\{i<6\}.$$

Contraejemplo o límites

No debe escribirse sin aclaración i=i+1 después de i:=i+1: los dos lados referirían al mismo estado. La sustitución o una variable histórica $i_0$ elimina esa ambigüedad.

Error típico: sustituir “hacia adelante”

La forma correcta parte de la postcondición $Q$. La regla falsa

$$\{P\}V:=E\{P_E^V\}$$

podría producir $\{x=0\}x:=1\{1=0\}$, lo cual revela el error. En cambio, para probar $\{?\}x:=1\{x=1\}$ se calcula $(x=1{)}_1^x$, que es $1=1$; por tanto la precondición más débil es $\top$.

Mini ejercicio

Para $z:=3x-2$ y $Q:z>7$:

$$(z>7{)}_{3x-2}^z\equiv 3x-2>7⟺x>3.$$

Comprueba con $x=4$ y con el valor frontera $x=3$.

Cálculo de una postcondición en las diapositivas

Cuando la precondición $P$ fija los valores necesarios para evaluar $E$, las diapositivas 26–27 llaman $C_{\{P\}}^E$ al resultado de sustituir esos valores en la igualdad $C\equiv (V=E)$:

$$\{P\}V:=E\left\{C_{\{P\}}^E\right\}.$$

En esa convención, $Q=C_{\{P\}}^E$. El esquema auxiliar $\{E=\{P\},C\}$ de las diapositivas indica el reemplazo que debe efectuarse; no representa una conjunción lógica.

Por ejemplo:

$$C_{\{a=3\}}^{4a}\equiv (k=4a{)}_{\{a=3\}}^{4a}\equiv k=12,$$

y por ello $\{a=3\}k:=4a\{k=12\}$. Esta es una sustitución hacia adelante de valores conocidos, no la forma general de la postcondición más fuerte para una precondición arbitraria.

Relaciones

• Calcula: Precondición más débil.
• Es una regla para: Terna de Hoare.
• Requiere distinguir: estado anterior y posterior.

Procedencia

• Clase: Ternas de Hoare y demostración formal.
• Fuente: Programación Avanzada Notas 4 2027, diapositivas 24–27 (láminas 78–81).
• Fuente complementaria: /Users/diegovillalba/Downloads/AllLectures.pdf, páginas PDF 14–16.
• Práctica interactiva: Asignación: sustituir desde la meta.