La operación que hace funcionar el ordenamiento por
mezcla. En cada vuelta sale el menor pendiente de las dos listas, y esa
regla tan simple esconde una pareja de invariantes igual a las de la clase
de ciclos: encuéntrelos y certifique el algoritmo con inicialización y
estabilidad.
1. Antes de ejecutar, prediga
Listas:
¿Cuántos elementos tendrá resultado al final?
2. Ejecute y mire las tres listas
Paso 0 de 0
Pruebe también las otras dos parejas de listas: en
una se agota primero la izquierda y quedan «sobras»; en la otra hay
empates y el <= decide quién sale primero.
3. La traza, copia por copia
Comparación
Sale
resultado
4. Los dos invariantes del primer while
Al comenzar cada vuelta, ¿qué es siempre
cierto de resultado? (ese será I₁)
¿Y las cotas de los índices? (ese será I₀)
5. La demostración, para el ciclo nuevo
Encuentre primero los
dos invariantes en la tarjeta 4.
Inicialización
Por las líneas 1–3: i = 0, j = 0 y
resultado = []. I₀: 0 ≤ 0 ≤ len(izq) y 0 ≤ 0 ≤ len(der). ✓ I₁:
la lista vacía contiene los 0 menores, en orden: cierto sin
esfuerzo. ✓
Estabilidad
Se asumen los invariantes antes de una vuelta
arbitraria. Hay dos casos, según cuál lista aporta el menor: si
izq[i] <= der[j] se copia izq[i], y en el otro caso der[j]. En ambos
se copia el menor de todos los pendientes, así que resultado sigue en
orden y ahora contiene los i + j + 1 menores; el índice de la lista que
aportó sube en 1 y sigue dentro de sus cotas, porque su lista aún tenía
elementos. Los invariantes son estables. ✓
Finalmente
Cada vuelta copia exactamente un elemento, así
que el primer while termina: alguna lista se agota. Por la estabilidad
de I₁, resultado contiene en orden los i + j menores; los pendientes de
la otra lista son los mayores y ya vienen ordenados, y los dos while
finales los copian. resultado queda completo y en orden: la
poscondición. Los invariantes son correctos. ∎
Así demuestra
CLRS la correctitud de su procedimiento Merge (pp. 31–33): con un
invariante de ciclo cuya estabilidad se revisa por casos. Las dos
técnicas del curso no compiten: la correctitud de la recursión se
argumenta por inducción estructural, y los invariantes certifican los
ciclos que quedan por dentro.
6. El costo
Mezclar dos listas con n elementos en total
cuesta: