Saltar al contenido
wandres.dev
Iniciar sesión

Modelo por capas

Lo que debe ser cierto entre operaciones

Una estructura guarda datos y también información sobre ellos: cuántos hay, dónde está el último, cuánto espacio queda. Esa información solo sirve si coincide con los datos.

Un invariante es una afirmación que debe ser cierta antes y después de cada operación. Durante la operación puede romperse un momento; al terminar, tiene que volver a cumplirse.

Para el chat de casilleros, escrito en el pseudocódigo de esta ruta (en él, x ← 5 significa «guarda 5 en x», a[i] es la posición i y nada es «ningún valor»):

Texto
los mensajes ocupan los casilleros 0 a cantidad − 1, sin huecoslos casilleros desde cantidad hasta el final están vacíoscantidad ≤ capacidad      (capacidad: cuántos casilleros hay)

En la figura, el chat tiene tres mensajes: cantidad vale 3 y marca el primer casillero libre.

Chat de casilleros con su invarianteCuatro casilleros, numerados de 0 a 3. Los casilleros 0, 1 y 2 contienen Hola, ¿Qué tal? y Bien; el casillero 3 está libre, con borde punteado. cantidad vale 3 y apunta al primer casillero libre; capacidad vale 4. Los mensajes ocupan los casilleros 0 a cantidad − 1, sin huecos.ocupados: casilleros 0 a cantidad − 1, sin huecosHola¿Qué tal?Bien0123cantidad = 3: primer casillero librecapacidad = 4: casilleros reservados
Con cantidad = 3 y capacidad = 4, los dos invariantes se cumplen: los tres mensajes están seguidos y 3 ≤ 4.

Cada operación tiene que dejar las dos ciertas.

borrar_último guarda el mensaje en una variable, baja cantidad y después vacía el casillero. Entre esas dos últimas líneas, cantidad ya bajó pero el casillero aún tiene el mensaje. ¿Cómo se juzga ese instante?