Pruebas basadas en propiedades: afirmar sobre todas las historias

Una prueba basada en propiedades no es una prueba con datos aleatorios, y confundir ambas cosas es la vía más rápida a una suite que tarda mucho y no encuentra nada. Es una construcción con tres piezas que se diseñan por separado y encajan por contrato: un generador, que sabe fabricar valores bien formados del dominio y muestrear el espacio con una distribución que tú controlas; un predicado, que es la propiedad enunciada como una función que devuelve verdadero o falso para cualquier valor generado; y un reductor, que ante un fallo busca el contraejemplo más pequeño que sigue fallando. El motor que las junta es de una simplicidad casi insultante y cabe en veinte líneas, cosa que conviene ver antes de usar una biblioteca, porque quien ha escrito el motor entiende luego qué está comprando. Lo difícil no es el motor: es escribir un predicado que prohíba algo de verdad y un generador cuya distribución alcance la región donde vive el fallo.

La anatomía de una propiedad

Un caso de prueba clásico tiene la forma de una afirmación existencial disfrazada: existe una entrada, la que escribí, para la que la salida es la que esperaba. Una propiedad tiene la forma que de verdad quieres afirmar: para todo valor v del dominio D, se cumple P de v. El cambio de forma trae una consecuencia inmediata sobre qué se puede escribir en la aserción. En un caso concreto puedes comparar contra un valor literal porque sabes cuál es. En una propiedad no lo sabes, así que la aserción debe expresar una relación que se mantenga sea cual sea el valor: una simetría, una invariante, una igualdad entre dos caminos distintos hacia el mismo sitio.

El motor recorre el dominio muestreándolo. Escribirlo entero deja claro que no hay magia y expone la pieza que decide todo lo demás, que es el generador pseudoaleatorio con semilla explícita.

// Generador determinista: la misma semilla reproduce exactamente la misma historia.
function motor(semilla) {
  let a = semilla >>> 0;
  return function siguiente() {
    a = (a + 0x6d2b79f5) >>> 0;
    let t = Math.imul(a ^ (a >>> 15), 1 | a);
    t = (t + Math.imul(t ^ (t >>> 7), 61 | t)) ^ t;
    return ((t ^ (t >>> 14)) >>> 0) / 4294967296;
  };
}

function paraTodo(nombre, generar, predicado, casos = 500) {
  for (let i = 0; i < casos; i += 1) {
    const semilla = 0x9e3779b9 ^ i;
    const valor = generar(motor(semilla));
    if (!predicado(valor)) return { nombre, ok: false, semilla, valor };
  }
  return { nombre, ok: true, casos };
}

La semilla explícita es la decisión de diseño más importante de este código y la que suele darse por sentada. Sin ella, una prueba que falla una vez de cada mil se convierte en un fantasma: aparece en integración continua, nadie consigue reproducirla, alguien la marca como inestable y el error queda enterrado bajo una anotación. Con ella, el informe de fallo contiene el número que regenera la historia exacta, y esa historia se convierte en el punto de partida de la reducción. Determinismo del generador y determinismo del sistema bajo prueba son ambos requisitos, no comodidades: si tu función de fusión consulta el reloj del sistema o un identificador aleatorio no sembrado, el contraejemplo no se reproduce y todo el nivel deja de funcionar.

Las leyes del semirretículo como aserciones

Antes de generar historias completas conviene comprobar las tres leyes que hacen que la fusión sea un supremo de semirretículo, porque son propiedades locales, baratas de generar y su violación explica de antemano casi cualquier divergencia posterior. Con el motor anterior se escriben en tres líneas cada una.

const gSet = {
  unir: (a, b) => new Set([...a, ...b]),
  iguales: (a, b) => a.size === b.size && [...a].every((x) => b.has(x)),
};

const conjunto = (r) => {
  const s = new Set();
  const n = Math.floor(r() * 6);
  for (let i = 0; i < n; i += 1) s.add(Math.floor(r() * 8));
  return s;
};
const trio = (r) => [conjunto(r), conjunto(r), conjunto(r)];

console.log(paraTodo('conmutativa', trio, ([a, b]) =>
  gSet.iguales(gSet.unir(a, b), gSet.unir(b, a))));

console.log(paraTodo('asociativa', trio, ([a, b, c]) =>
  gSet.iguales(gSet.unir(gSet.unir(a, b), c), gSet.unir(a, gSet.unir(b, c)))));

console.log(paraTodo('idempotente', trio, ([a]) =>
  gSet.iguales(gSet.unir(a, a), a)));

Hay un detalle en el generador que parece menor y decide la potencia de las tres pruebas: el rango de valores es de ocho y el tamaño máximo del conjunto es de seis. Esa estrechez es deliberada. Si los valores se tomasen de un espacio grande, los conjuntos generados serían casi siempre disjuntos y las tres leyes se cumplirían trivialmente sin ejercitar ninguna interacción. Las propiedades algebraicas se rompen en el solapamiento, de modo que el generador debe forzar colisiones a propósito. Es el primer ejemplo de una regla general del nivel: un generador uniforme sobre un dominio ancho es casi siempre un mal generador.

Qué genera el motor y cómo se gobierna

Las leyes locales son el aperitivo. La propiedad que da nombre al nivel es la de extremo a extremo: para toda historia bien formada, cuando todos los mensajes se han entregado, todas las réplicas coinciden. El generador ya no produce conjuntos sueltos sino programas: listas de eventos que un simulador ejecutará.

flowchart LR
S[semilla] --> G[generador de historias]
G --> H[historia bien formada]
H --> E[simulador de replicas y red]
E --> Q[estado de reposo]
Q --> P[predicado de convergencia]
P -->|verdadero| S
P -->|falso| R[reductor de casos]
R --> C[contraejemplo minimo]
style P fill:#89b4fa,color:#11111b
style C fill:#a6e3a1,color:#11111b

Sobre la palabra bien formada descansa buena parte del trabajo. Una historia mal formada es la que el sistema no podría haber producido nunca: una entrega de un mensaje que aún no se ha enviado, un borrado de un elemento que ninguna réplica insertó, una entrega dirigida a la réplica que la originó. Generar esas historias no encuentra errores sino que produce falsos positivos, y el tiempo se va en descartarlos. Hay dos maneras de evitarlas y su diferencia de coste es enorme.

Filtrar   generar libremente y descartar lo que no cumple la precondicion
          coste alto si la precondicion es estrecha, y muchas historias tiradas

Construir generar solo historias validas por construccion, eligiendo cada
          evento entre los que son legales en el estado actual del generador
          coste bajo y control total sobre la distribucion

La segunda vía es casi siempre la correcta en este dominio y tiene una consecuencia que conviene anticipar: el generador acaba siendo un modelo del sistema, con su propia noción de qué mensajes hay en vuelo y qué elementos existen. Ese modelo es código que hay que mantener y que puede tener errores propios, y es el precio de admisión de la técnica.

Queda una pieza de gobierno que se omite muy a menudo y que es la única forma honesta de saber si el generador hace lo que crees. Consiste en clasificar los casos generados y publicar la estadística junto al resultado: qué fracción de las historias tuvo concurrencia real, cuántas incluyeron un borrado seguido de una reinserción concurrente, cuántas terminaron con la red vacía. Sin esa tabla, una propiedad que pasa quinientas veces no distingue entre un sistema correcto y un generador que produjo quinientas historias secuenciales.

El sesgo del generador es tu punto ciego

Toda la técnica descansa sobre una premisa que casi nunca se enuncia: el fallo está dentro de la región del espacio que tu generador puede alcanzar. Fuera de ella, la propiedad no dice nada, y no lo dice en silencio, con el mismo color verde con el que informa de sus éxitos. El generador no es un detalle de implementación sino la parte de la prueba que decide qué se puede descubrir, y por eso merece revisión de código con el mismo cuidado que el algoritmo.

Los sesgos más caros son de tres tipos. El de longitud, cuando las historias son tan cortas que nunca hay tres operaciones concurrentes sobre el mismo elemento, o tan largas que el estado se satura y las últimas operaciones ya no cambian nada. El de dominio, cuando el rango de valores o de identificadores es tan ancho que nunca se producen colisiones, que es donde viven los desempates. Y el estructural, el peor de todos, cuando el generador solo sabe producir la forma de historia que su autor tenía en la cabeza, típicamente dos réplicas que alternan ordenadamente, sin ráfagas, sin silencios largos y sin una tercera réplica que llegue tarde con información antigua.