Caso real

Las pruebas de propiedades

Muchos equipos prueban sus estructuras generando miles de secuencias de operaciones al azar y comprobando el invariante después de cada una. Cuando falla, la herramienta reduce la secuencia hasta la más corta que reproduce el error. Es la forma más eficaz de encontrar el «error que aparece en otra operación».

Imagina que escribes una prueba así para el chat de casilleros: qué comprobarías después de cada operación.

Escribes una prueba de propiedades para el chat de casilleros. Genera secuencias al azar de agregar y borrar_último, y quieres comprobar algo después de cada operación. ¿Qué propiedad compruebas?Que la última operación terminó sin error, porque todo invariante roto lanza un error al instanteQue cantidad es igual al número de agregar ejecutados hasta ahora, porque cada agregar suma unoQue el último mensaje agregado sigue en el casillero cantidad − 1, porque agregar lo puso ahíQue cantidad ≤ capacidad y que los casilleros 0 a cantidad − 1 estén llenos y el resto vacíos