Recorrido narrado

Leer una operación con su invariante

Una forma útil de leer cualquier operación: preguntar, línea a línea, si el invariante se cumple al final.

función agregar(chat, m):    si cantidad = capacidad:        error "lleno"          # el invariante cantidad ≤ capacidad sigue en pie    casilleros[cantidad] ← m   # m queda justo después del último: sin hueco    cantidad ← cantidad + 1    # ahora los mensajes ocupan 0 a cantidad − 1

En la figura, el chat tiene capacidad 5 y agregas «Nos vemos». Debajo, el mismo caso con las dos últimas líneas al revés.

Si cambias el orden de las dos últimas líneas, m se escribe un casillero más allá y deja un hueco. Cada línea está ahí para proteger el invariante.

En esta ruta, cada estructura tendrá sus invariantes nombrados: el orden de un árbol de búsqueda, la cola de una lista, el orden de un heap. La mayoría de los errores de implementación son invariantes que una operación olvidó mantener.