Invariantes y por qué un ciclo funciona

Probar un ciclo con cinco ejemplos no explica por qué funcionará con el sexto. Una invariante sí: nombra algo que permanece verdadero durante toda la repetición y conecta cada paso con el resultado final.

Una suma acumulada, y qué se afirma de ella

Consideremos una suma acumulada:

let total = 0;
for (let index = 0; index < values.length; index += 1) {
  total += values[index];
}

La invariante es: al comenzar cada iteración, total contiene la suma de los elementos en posiciones anteriores a index. Describe con precisión qué parte ya está resuelta.

Inicialización: verdadera antes de la primera vuelta

Primero demostramos inicialización. Antes de la primera vuelta, index vale cero y no hay elementos anteriores. La suma vacía es cero, exactamente el valor inicial de total.

Una invariante mal elegida suele fallar acá. Si afirmáramos que total ya incluye la posición actual, sería falso antes de ejecutar el cuerpo por primera vez.

Mantenimiento: si entra verdadera, sale verdadera

Después suponemos que la afirmación es cierta al entrar a una vuelta. El cuerpo agrega values[index] y el avance incrementa index. Al comenzar la vuelta siguiente, total incluye exactamente todas las posiciones anteriores al nuevo índice.

No asumimos el resultado final. Demostramos que un estado válido produce el siguiente estado válido; por eso el razonamiento se extiende a cualquier cantidad de iteraciones.

Salida: la invariante más la condición dan el resultado

Cuando el ciclo termina, index es igual a values.length. La invariante dice entonces que total suma todas las posiciones anteriores a la longitud: todo el arreglo. Invariante más condición de salida implican la postcondición.

La corrección se completa justificando terminación: el índice crece en uno, tiene una cota y no puede avanzar indefinidamente.

La invariante también sirve para diseñar

Las invariantes también sirven para diseñar. Preguntá qué debería significar el estado justo antes de cada vuelta; luego elegí inicialización, cuerpo y condición para conservar ese significado.

En búsqueda binaria, el objetivo —si existe— permanece dentro del intervalo activo. En ordenamiento por inserción, el prefijo anterior al índice permanece ordenado. Nombrar esa propiedad revela qué debe hacer el próximo paso.

Escribirla como aserción

const maxOf = (values: readonly number[]): number => {
  if (values.length === 0) throw new Error('maxOf necesita al menos un valor');

  let best = values[0]!;
  let index = 1;

  while (index < values.length) {
    // invariante: best es el mayor de values[0..index-1]
    console.assert(
      values.slice(0, index).every((value) => value <= best),
      'la invariante de maxOf se rompió',
    );

    if (values[index]! > best) best = values[index]!;
    index += 1;
  }

  // al salir, index === values.length, así que best es el mayor de todo
  return best;
};

La aserción dice exactamente la misma frase que la invariante escrita en castellano, y por eso no puede quedar desactualizada: si alguien cambia el ciclo y la rompe, salta. En una versión de producción esa línea se saca o se compila fuera, y en desarrollo vale mucho más que un comentario.

El comentario del final es la otra mitad del argumento: al salir, la condición del while es falsa, o sea index === values.length, y la invariante con ese valor dice justo lo que la función promete devolver. Los ciclos correctos se demuestran así, y la demostración cabe en dos líneas.

Para qué sirve escribirla

Un ciclo es correcto si se cumplen tres cosas: la invariante vale antes de la primera vuelta —inicialización—, cada vuelta la conserva —mantenimiento—, y al terminar, la invariante junto con la condición de salida dan lo que se quería —terminación—. Escribir esas tres líneas encuentra más errores que probar con ejemplos, porque los ejemplos sólo cubren los casos que a uno se le ocurrieron.

Cierre

Una prueba de ciclo tiene cuatro piezas: invariante, inicialización, mantenimiento y salida; además necesita progreso para terminar. No es formalismo decorativo: es una herramienta para encontrar la estructura correcta antes de escribir el cuerpo.