Verificación de la implementación

01 · Punto de partida

Del «corre» al «obedece»

Que el programa ejecute sin excepciones no prueba nada: un índice corrido, una cola atendida en orden inverso o una semilla reusada también «corren». La verificación de la implementación pregunta algo más duro:

• ¿Cada línea ejecuta la regla auditada en el Tema 2?
• ¿Los eventos ocurren en el orden y el instante correctos?
• ¿El azar es reproducible y no contamina entre réplicas?
• ¿Qué evidencia guardás de que todo eso se cumple?

02 · Definición

Qué se verifica y con qué oracle

Cada verificación necesita un oráculo: una fuente independiente de la respuesta correcta.

03 · Técnicas

La caja de herramientas del verificador

1. 1
   Pruebas unitarias con asserts.

   Una función, una regla, un valor esperado exacto. Se ejecutan siempre, en cada cambio. Son la red de seguridad.

2. 2
   Trazas de eventos.

   Registrar (t, evento, estado antes → después) en las primeras corridas. Leer 10 líneas de traza revela órdenes imposibles.

3. 3
   Chequeo de invariantes en caliente.

   Afirmar en cada paso que 0 ≤ nivel ≤ tope y que el tiempo avanza. Si algo lo viola, el programa se detiene con mensaje, no sigue mintiendo.

4. 4
   Semilla fija y aislamiento del azar.

   Un generador por réplica, creado con su semilla. Nada de random global compartido ni de usar la hora como semilla en tests.

5. 5
   Regresión y revisión de código.

   Guardar una historia «dorada» y compararla en cada cambio. Otra persona lee el diff preguntando «¿qué regla del papel ejecuta esta línea?».

04 · Defectos típicos

Los sospechosos habituales

Unidades en el código

La spec dice litros/paso pero el código suma litros/minuto. Mismo defecto del Tema 2, ahora en la traducción a código.

Flotantes y comparaciones

Comparar nivel == 0 con flotantes en vez de tolerancia o de <= 0. El invariante debe usar margen.

Estado global

Listas o generadores que sobreviven entre llamadas. Cada corrida debe partir de una construcción fresca.

05 · Representación en Python

Tests, traza e invariantes en código

Una implementación verificada no es solo la función que simula: es la función más su suite de chequeos. Este es el molde mínimo.

def simular(nivel_inicial, entrada, salida, tope, pasos, traza=None):
    nivel = nivel_inicial
    historia = []
    for t in range(1, pasos + 1):
        antes = nivel
        nivel = min(tope, max(0, nivel + entrada - salida))
        # Invariante en caliente: el programa se acusa a sí mismo
        assert 0 <= nivel <= tope, f"invariante roto en t={t}: {nivel}"
        assert t == len(historia) + 1, "tiempo fuera de orden"
        historia.append(nivel)
        if traza is not None:
            traza.append((t, antes, entrada, salida, nivel))
    return historia

# Suite de verificación (oráculos exactos, sin datos reales)
assert simular(10, 3, 2, 14, 3) == [11, 12, 13]
assert simular(5, 4, 4, 14, 3) == [5, 5, 5]
assert simular(2, 1, 3, 14, 3) == [0, 0, 0]
assert simular(14, 3, 2, 14, 2) == [14, 14]
assert len(simular(10, 3, 2, 14, 12)) == 12
print("Suite OK: 5/5 tests exactos")

La suite tarda milisegundos y se ejecuta en cada cambio. Ese es el punto: verificación barata y continua.

Traza legible + determinismo del azar

import random

def replica_con_azar(semilla, pasos):
    rng = random.Random(semilla)  # un generador por réplica, aislado
    nivel, historia = 10, []
    for t in range(pasos):
        llegada = rng.choice([2, 3, 4])  # azar controlado
        nivel = max(0, min(14, nivel + llegada - 2))
        historia.append(nivel)
    return historia

traza = []
print(simular(10, 3, 2, 14, 3, traza=traza))
for t, antes, e, s, despues in traza:
    print(f"t={t}: {antes} +{e}-{s} -> {despues}")

a = replica_con_azar(42, 6)
b = replica_con_azar(42, 6)
print("determinista:", a == b, a)

06 · Exploración

Laboratorio: suite de verificación en vivo

Este simulador de tanque esconde dos interruptores de bug: desfase de un paso (off-by-one) y olvido del piso (permite negativos). Mové la entrada y activá cada bug para ver qué tests de la suite caen y cómo la curva naranja se separa de la esperada (lima).

La curva lima es la historia que la especificación promete. La curva naranja es lo que el programa calcula con los bugs activados. Los puntos rojos marcan pasos donde el invariante 0 ≤ nivel ≤ tope se viola.

Preguntas para explorar

1. Activá el desfase con entrada 3 y salida 2. ¿Cuántos tests caen? ¿Por qué un error de un paso contamina toda la historia?
2. Activá «olvidar el piso» con entrada 1 y salida 4. ¿Dónde aparecen los negativos? ¿Qué test los caza aunque el balance parezca razonable?
3. ¿Por qué la suite usa valores exactos y no tolerancias? ¿Qué pasaría si validaras (con MAE) un programa con desfase?

07 · Comprensión

Confusiones frecuentes

08 · Práctica guiada

Ejercicios con Python

Ejercicio 1: cazar el off-by-one

Esta función devuelve un paso de más. Escribí el assert que la delata.

def sim_off(nivel, entrada, salida, pasos):
    h = []
    for t in range(pasos + 1):  # BUG: un paso de más
        nivel = max(0, nivel + entrada - salida)
        h.append(nivel)
    return h

print(len(sim_off(10, 3, 2, 3)))
print("assert len(...) == 3:", len(sim_off(10, 3, 2, 3)) == 3)

Ejercicio 2: invariante que grita

Agregá el invariante que detiene esta simulación en cuanto el nivel se vuelve imposible.

def sim_sin_piso(nivel, entrada, salida, pasos):
    h = []
    for t in range(pasos):
        nivel = nivel + entrada - salida  # sin max(0, ...)
        assert 0 <= nivel, f"invariante roto en t={t+1}: nivel={nivel}"
        h.append(nivel)
    return h

print(sim_sin_piso(2, 1, 3, 2))

Ejercicio 3: determinismo entre réplicas

Dos réplicas con la misma semilla deben coincidir; con distinta semilla, casi seguro no. Comprobalo.

import random
def replica(semilla):
    rng = random.Random(semilla)
    return [rng.choice([2, 3, 4]) for _ in range(5)]

print(replica(7) == replica(7))  # True: determinista
print(replica(7) == replica(8))  # casi seguro False: independientes

09 · Síntesis

Ideas para recordar

En el próximo tema veremos la depuración de simulaciones: técnicas sistemáticas para encontrar y aislar el bug cuando la suite se pone roja.