El primer ciclo de la clase. Prediga qué devuelve, mire la
traza de estados y descubra las dos propiedades que ninguna vuelta rompe:
los invariantes I₀ e I₁. Con ellos, la demostración de correctitud sale en
tres movimientos: inicialización, estabilidad y el cierre.
1. La especificación y la predicción
Entrada: un arreglo A[0..N) de números,
N ≥ 0. Salida: A[0] + A[1] + … + A[N−1].
Arreglo:
¿Qué devuelve sumarArreglo(A)?
2. Ejecute y mire
Paso 0 de 0
Cada vez que la ejecución pasa por la línea 3, el
while evalúa su condición: esa foto de (i, ac) es un «chequeo» y
queda en la tabla de abajo.
3. La traza por estados
Chequeo
i
ac
¿Qué se repite?
4. Los dos invariantes
Todo cambia de fila en fila, pero dos propiedades
se cumplen en todas, incluida la primera y la última.
¿Qué lleva ac 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. El teorema a demostrar es el de la
clase: Teorema 1 — los invariantes I₀ e I₁ se cumplen.
Inicialización: según las líneas 1–2, ¿cuál es el estado inicial (i, ac)?
Para I₀: 0 ≤ 0 ≤ N. ✓ Para I₁:
ac = A[0] + … + A[−1] es una suma sobre el rango vacío [0..0), que vale
0 = ac. ✓ Los dos 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 0 ≤ j ≤ N y ac = A[0] + … + A[j−1]. Al
ejecutar las líneas 4–5: ac = (A[0] + … + A[j−1]) + A[j] =
A[0] + … + A[j], e i = j + 1: exactamente I₁ evaluado en j + 1. E I₀
vale porque j < N implica 0 ≤ j + 1 ≤ N. 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 llegar a N. Por la estabilidad de I₁, al terminar:
ac = A[0] + … + A[N−1], lo que coincide con la poscondición. Los
invariantes son correctos. ∎
Teorema 2. La invocación sumarArreglo(A) para
cualquier arreglo A produce la suma de sus elementos.
Demostración: es trivial a partir de la correctitud de los
invariantes I₀ e I₁. ∎