En sumarArreglo los invariantes se descubrieron con calma.
Aquí el recorrido es el mismo —predecir, ejecutar, proponer I₀ e I₁,
demostrar con inicialización y estabilidad— pero las decisiones son suyas.
Al final, un experimento con una entrada que no cumple la precondición.
1. La especificación y la predicción
Entrada: N ∈ ℕ. Salida: N!
N = 5
¿Qué devuelve fact(5)?
2. Ejecute y mire
Paso 0 de 0
La foto (i, ans) se toma en cada chequeo del while.
Ojo con la condición: aquí es i <= N, no i < N.
3. La traza por estados
Chequeo
i
ans
¿Qué se repite?
4. Los dos invariantes
¿Qué lleva ans en función de i? (ese será I₁)
¿Entre qué valores se mueve i en los chequeos? (ese será I₀)
5. La demostración
Encuentre primero los
dos invariantes en la tarjeta 4.
Inicialización: por las líneas 1–2, (i, ans) = (1, 1). Para I₁ hace falta saber: ¿cuánto es 0!?
Para I₀: 1 ≤ 1 ≤ N + 1. ✓ Para I₁:
ans = (1 − 1)! = 0! = 1. ✓ Los invariantes se cumplen en la
inicialización.
Estabilidad
Se considera una iteración arbitraria i = j (con
j ≤ N: de lo contrario el cuerpo no se habría ejecutado) y se asume que
antes de ella valen 1 ≤ j ≤ N + 1 y ans = (j − 1)!. Al ejecutar las
líneas 4–5: ans = (j − 1)! · j = j!, e i = j + 1: exactamente I₁
evaluado en j + 1. E I₀ vale porque j ≤ N implica 1 ≤ j + 1 ≤ N + 1.
Los invariantes son estables. ✓
Finalmente: ¿con qué valor de i termina el ciclo?
El ciclo terminará ya que i se incrementa de 1
en 1 hasta superar a N. Por la estabilidad de I₁, al terminar:
ans = (N + 1 − 1)! = N!, y eso es lo que llega a la línea 6. Los
invariantes son correctos. ∎
Teorema 2. La invocación fact(N) para cualquier
N ≥ 0 produce como resultado N!. Demostración: es trivial
a partir de la correctitud de los invariantes I₀ e I₁. ∎
6. El experimento: salirse de la precondición
La especificación pide N ∈ ℕ. ¿Y si alguien llama
fact(-1)?
La condición
1 ≤ −1 falla desde el primer chequeo: el ciclo no corre y la función
devuelve 1. ¿Está mal el algoritmo? No: −1 no es una instancia del
problema, porque no cumple la precondición N ∈ ℕ. La correctitud se
promete para las entradas que cumplen las precondiciones; para las demás
no se promete nada. (Y note que fact(0) sí es una instancia:
devuelve 1 = 0!, como debe ser.)