La lógica de Hoare proporciona una prueba o un contraejemplo

Question

Me he encontrado con una pregunta en la que se pedía una prueba en forma de tabla: $\{x>1\} a=1; y=x; y=y-a \{y>0 \wedge x>y\}$

Creo que es falso pero no se me ocurre un contraejemplo de ello.

Answer 1

Por Regla de Asignación, tienes:

$\{ x > 1 \} a = 1 \{ a = 1\land x > 1\}$

y

$\{ a = 1\land x > 1 \} y = x \{ a = 1\land x > 1\land y = x\}$

y

$\{ a = 1\land x > 1\land y = x\} y = y - a \{ a = 1 \land x > 1\land y = x-1 \}$

Ahora puedes utilizar la Regla de la Composición dos veces para convertirla en:

$\{ x > 1 \} a = 1; y = x; y = y - a \{ a = 1\land x > 1\land y = x-1 \}$

que por lógica y aritmética básica significa:

$\{ x > 1 \} a = 1; y = x; y = y - a \{ a = 1\land y > 0\land x > y \}$

Por supuesto, todo el trabajo interesante lo hace la parte de "lógica y aritmética básica". La lógica de Hoare en sí misma no está haciendo mucho de interés para esta 'prueba' en absoluto.

Nota: Es la primera vez que veo la Lógica de Hoare, así que estoy tratando de entenderla a partir de la Wikipedia... ¡los que sepan de lógica de Hoare, por favor, destrocen este post si contiene errores!