Lógica de Hoare · práctica guiada

Elige un tipo de programa y avanza un paso a la vez. La ejecución va hacia adelante; la verificación de asignaciones suele construirse hacia atrás.

Precondición más débil de una secuencia

x := x + 1;
y := 2 * x

Postcondición: y ≥ 10
Regla: wp(V := E, Q) = Q[E/V]. Se comienza por la última instrucción.

Las dos ramas deben llegar a la misma meta

if x ≥ 0 then
    y := x
else
    y := -x

Postcondición: y ≥ 0
Regla: se prueba la rama verdadera con P ∧ B y la falsa con P ∧ ¬B.

Suma de 1 hasta n

i := 0; s := 0;
while i < n do
    i := i + 1;
    s := s + i

Post: s = n(n+1)/2
Iteración0
i0
s0