Aprende cómo el trabajo de Tony Hoare sobre la lógica de Hoare, Quicksort y la mentalidad de seguridad moldeó técnicas prácticas para escribir y revisar software correcto.
Cuando la gente dice que un programa es “correcto”, a menudo quiere decir: “Lo ejecuté unas cuantas veces y la salida parecía correcta”. Eso es una señal útil, pero no es corrección. En términos llanos, corrección significa que el programa cumple su especificación: para cada entrada permitida, produce el resultado requerido y respeta las reglas sobre cambios de estado, tiempos y errores.
La trampa es que “cumplir su spec” es más difícil de lo que parece.
Primero, las especificaciones suelen ser ambiguas. Un requisito de producto puede decir “ordenar la lista”, pero ¿significa eso ordenamiento estable? ¿Y los valores duplicados, las listas vacías o los elementos no numéricos? Si la spec no lo dice, distintas personas asumirán respuestas distintas.
Segundo, los casos límite no son raros: simplemente se prueban con menos frecuencia. Valores nulos, desbordes, límites off-by-one, secuencias de usuario inusuales y fallos externos inesperados pueden convertir “parece que funciona” en “falló en producción”.
Tercero, los requisitos cambian. Un programa puede ser correcto respecto a la spec de ayer e incorrecto respecto a la de hoy.
La gran contribución de Tony Hoare no fue reclamar que debiéramos probarlo todo todo el tiempo. Fue la idea de que podemos ser más precisos sobre lo que el código debe hacer y razonar sobre ello de forma disciplinada.
En esta entrada seguiremos tres hilos conectados:
La mayoría de los equipos no escribirán pruebas formales completas. Pero incluso el pensamiento parcial “al estilo prueba” puede facilitar detectar bugs, afinar las revisiones y aclarar comportamiento antes de que el código se despliegue.
Tony Hoare es uno de esos raros científicos de la computación cuyo trabajo no se quedó en artículos o aulas. Se movió entre la academia y la industria, y se preocupó por una pregunta práctica que todo equipo sigue enfrentando: ¿cómo sabemos que un programa hace lo que creemos que hace, especialmente cuando hay mucho en juego?
Este artículo se centra en algunas ideas de Hoare que aparecen una y otra vez en bases de código reales:
{P} C {Q}.No encontrarás formalismo matemático profundo aquí, y no intentaremos una prueba completa verificable por máquina de Quicksort. El objetivo es mantener los conceptos accesibles: la estructura suficiente para que tu razonamiento sea más claro, sin convertir la revisión de código en un seminario de posgrado.
Las ideas de Hoare se traducen en decisiones ordinarias: de qué suposiciones depende una función, qué garantiza al llamador, qué debe mantenerse cierto a mitad de un bucle y cómo detectar cambios “casi correctos” durante las revisiones. Incluso si nunca escribes {P} C {Q} explícitamente, pensar en esa forma mejora las APIs, las pruebas y la calidad de las discusiones sobre código complicado.
La visión de Hoare es más estricta que “pasó algunos ejemplos”: la corrección trata de cumplir una promesa acordada, no de parecer correcta en una muestra pequeña.
Los bugs suelen aparecer cuando los equipos se saltan el paso intermedio: pasan de requisitos a código dejando la “promesa” difusa.
Dos afirmaciones distintas que con frecuencia se mezclan:
Para sistemas reales, “nunca terminar” puede ser tan dañino como “terminar con la respuesta equivocada”.
Las afirmaciones de corrección nunca son universales; dependen de suposiciones sobre:
Hacer explícitas las suposiciones convierte “funciona en mi máquina” en algo que otros pueden razonar.
Considera una función sortedCopy(xs).
Una spec útil podría ser: “Devuelve una nueva lista ys tal que (1) ys está ordenada en orden ascendente, y (2) ys contiene exactamente los mismos elementos que xs (mismas cuentas), y (3) xs permanece sin cambios.”
Ahora “correcto” significa que el código satisface esos tres puntos bajo las suposiciones indicadas—no solo que la salida parece ordenada en una prueba rápida.
La lógica de Hoare es una manera de hablar del código con la misma claridad que usarías para un contrato: si empiezas en un estado que satisface ciertas suposiciones y ejecutas este fragmento de código, acabarás en un estado que satisface ciertas garantías.
La notación central es el triple de Hoare:
{precondición} programa {postcondición}
Una precondición indica lo que debe ser cierto antes de ejecutar el fragmento de programa. No se trata de lo que esperas que sea cierto; es lo que el código necesita que sea cierto.
Ejemplo: supongamos que una función devuelve el promedio de dos números sin comprobaciones de desbordamiento.
a + b cabe en el tipo enteroavg = (a + b) / 2avg es el promedio matemático de a y bSi la precondición no se cumple (es posible desbordamiento), la promesa de la postcondición deja de aplicar. El triple te obliga a decirlo en voz alta.
Una postcondición indica lo que será cierto después de ejecutar el código—asumiendo que la precondición se cumplió. Buenas postcondiciones son concretas y comprobables. En lugar de decir “el resultado es válido”, explica qué significa “válido”: ordenado, no negativo, dentro de límites, inalterado salvo campos específicos, etc.
La lógica de Hoare escala desde sentencias diminutas hasta código multi-paso:
x = x + 1, ¿qué hechos sobre x son ahora ciertos?El objetivo no es esparcir llaves por todas partes, sino hacer la intención legible: suposiciones claras, resultados claros y menos conversaciones de “parece que funciona” en las revisiones.
Un invariante de bucle es una afirmación que es cierta antes de que comience el bucle, permanece cierta después de cada iteración y sigue siendo cierta cuando el bucle finaliza. Es una idea simple con gran impacto: reemplaza “parece que funciona” por una afirmación que puedes comprobar en cada paso.
Sin un invariante, una revisión suele sonar así: “Iteramos la lista y gradualmente arreglamos cosas.” Un invariante obliga a la precisión: qué exactamente ya es correcto ahora, aunque el bucle no haya terminado. Una vez que puedas decir eso con claridad, errores off-by-one y casos faltantes resultan más fáciles de detectar, porque se verán como momentos en que el invariante quedaría roto.
La mayoría del código del día a día puede usar unas pocas plantillas fiables.
1) Límites / seguridad de índices
Mantener índices en un rango seguro.
0 <= i <= nlow <= left <= right <= highEste tipo de invariante es excelente para prevenir accesos fuera de rango y para hacer el razonamiento sobre arreglos concreto.
2) Elementos procesados vs. no procesados
Divide tus datos en una región “hecha” y una “por hacer”.
a[0..i) han sido examinados.”result satisface el predicado de filtro.”Esto convierte el progreso vago en un contrato claro sobre qué significa “procesado”.
3) Prefijo ordenado (o prefijo particionado)
Común en ordenamientos, fusiones y particionados.
a[0..i) está ordenado.”a[0..i) son <= pivot, y todos los elementos en a[j..n) son >= pivot.”Aunque el arreglo completo no esté ordenado aún, has fijado lo que sí lo está.
La corrección no es solo estar en lo cierto; el bucle también debe terminar. Una forma simple de argumentarlo es nombrar una medida (a menudo llamada variante) que disminuye en cada iteración y no puede disminuir indefinidamente.
Ejemplos:
n - i se reduce en 1 cada vez.”Si no puedes encontrar una medida que se reduzca, puede que hayas descubierto un riesgo real: un bucle infinito en algunas entradas.
Quicksort tiene una promesa simple: dada una porción (slice) o segmento de arreglo, rearrange sus elementos para que queden en orden no decreciente, sin perder ni inventar valores. La forma general del algoritmo es fácil de resumir:
Es un gran ejemplo para enseñar corrección porque es lo suficientemente pequeño para mantener en la cabeza, pero suficientemente rico para mostrar dónde falla el razonamiento informal. Un Quicksort que “parece funcionar” con algunas pruebas aleatorias puede estar equivocado en formas que solo aparecen con entradas o condiciones límite específicas.
Algunos problemas causan la mayoría de bugs:
Para argumentar corrección al estilo Hoare, normalmente separas la prueba en dos partes:
Esta separación mantiene el razonamiento manejable: consigue que la partición esté bien, y luego construye la corrección del ordenamiento sobre ella.
La velocidad de Quicksort depende de una rutina engañosamente pequeña: la partición. Si la partición está aunque sea ligeramente mal, Quicksort puede desordenar, entrar en bucle infinito o fallar en casos límite.
Usaremos el clásico esquema de partición de Hoare (dos punteros que se mueven hacia el interior).
Entrada: un fragmento de arreglo A[lo..hi] y un valor pivot elegido (a menudo A[lo]).
Salida: un índice p tal que:
A[lo..p] es <= pivotA[p+1..hi] es >= pivotFíjate en lo que no se promete: el pivote no necesariamente queda en la posición p, y los elementos iguales al pivote pueden aparecer a ambos lados. Eso está bien: Quicksort solo necesita una separación correcta.
Mientras el algoritmo avanza dos índices—i desde la izquierda y j desde la derecha—el razonamiento útil se centra en lo que ya está “cerrado”. Un conjunto práctico de invariantes es:
A[lo..i-1] son <= pivot (el lado izquierdo está limpio)A[j+1..hi] son >= pivot (el lado derecho está limpio)A[i..j] está sin clasificar (aún por comprobar)Cuando encontramos A[i] > pivot y A[j] < pivot, intercambiarlos preserva esas invariantes y reduce la porción sin clasificar.
i avanza hacia la derecha; la partición debe terminar y devolver un p sensato.j avanza hacia la izquierda; misma preocupación de terminación.< vs <=), los punteros pueden quedarse sin avanzar. El esquema de Hoare depende de una regla consistente para que el progreso continúe.Existen distintos esquemas de partición (Lomuto, Hoare, partición tres-vías). La clave es elegir uno, declarar su contrato y revisar el código según ese contrato de forma consistente.
La recursión es más fácil de confiar cuando puedes responder dos preguntas claramente: ¿cuándo para? y ¿por qué cada paso es válido? El pensamiento al estilo Hoare ayuda porque te obliga a decir qué debe ser cierto antes de una llamada y qué será cierto después de que retorne.
Una función recursiva necesita al menos un caso base donde no hace más llamadas recursivas y aún así satisface el resultado prometido.
Para ordenación, un caso base típico es “arreglos de longitud 0 o 1 ya están ordenados”. Aquí, “ordenado” debe ser explícito: para una relación de orden ≤, la salida está ordenada si para cada índice i < j se cumple a[i] ≤ a[j]. (Que los elementos iguales conserven su orden original es otra propiedad llamada estabilidad; Quicksort normalmente no es estable salvo que se diseñe para ello.)
Cada paso recursivo debe llamar sobre una entrada estrictamente menor. Esta “reducción” es tu argumento de terminación: si el tamaño disminuye y no puede bajar de 0, no puedes recursar para siempre.
La reducción también importa por seguridad de pila. Incluso el código correcto puede fallar si la profundidad de recursión es demasiado grande. En Quicksort, particiones muy desbalanceadas pueden producir recursión profunda. Eso es una prueba de terminación más un recordatorio práctico para considerar la profundidad peor caso.
El peor caso temporal de Quicksort puede degradarse a O(n²) cuando las particiones son muy desbalanceadas, pero eso es un problema de rendimiento, no de corrección. El objetivo del razonamiento aquí es: asumiendo que la partición preserva los elementos y los divide según el pivote, ordenar recursivamente las subpartes implica que el arreglo completo satisface la definición de ordenamiento.
Las pruebas y el razonamiento al estilo prueba buscan el mismo objetivo—confianza—pero lo alcanzan de formas distintas.
Las pruebas son excelentes para atrapar errores concretos: un off-by-one, un caso límite faltante, una regresión. Pero una suite de pruebas solo puede muestrear el espacio de entradas. Incluso “100% de cobertura” no significa “todas las conductas verificadas”; significa mayormente “todas las líneas ejecutadas”.
El razonamiento al estilo prueba (particularmente el estilo Hoare) parte de una especificación y pregunta: si estas precondiciones se cumplen, ¿el código siempre establece las postcondiciones? Cuando se hace bien, no solo encuentras un bug: a menudo puedes eliminar una categoría entera de errores (como “acceso fuera de rango” o “el bucle rompe la propiedad de partición”).
Una spec clara es un generador de pruebas.
Si tu postcondición dice “la salida está ordenada y es una permutación de la entrada”, automáticamente obtienes ideas de prueba:
La spec te dice qué significa “correcto” y las pruebas verifican que la realidad coincide.
Las pruebas basadas en propiedades se sitúan entre las pruebas y las pruebas formales. En vez de seleccionar casos a mano, expresas propiedades y dejas que una herramienta genere muchas entradas.
Para ordenamiento, dos propiedades simples funcionan muy bien:
Estas propiedades son esencialmente postcondiciones escritas como comprobaciones ejecutables.
Una rutina ligera que escala:
Si quieres institucionalizarlo, agrega “spec + notas de razonamiento + pruebas” a tu plantilla de PR o checklist de revisión de código (ver también /blog/code-review-checklist).
Si usas un flujo de trabajo de generación rápida de código (vibe-coding) desde una interfaz tipo chat, la misma disciplina aplica—posiblemente más. En Koder.ai, por ejemplo, puedes empezar en modo Planning para fijar precondiciones/postcondiciones antes de generar código, luego iterar con snapshots y rollback mientras añades tests basados en propiedades. La herramienta acelera la implementación, pero la spec sigue siendo lo que evita que “rápido” se convierta en “frágil”.
La corrección no trata solo de “el programa devuelve el valor correcto”. El pensamiento de seguridad plantea otra pregunta: ¿qué resultados son inaceptables y cómo los prevenimos, incluso cuando el código está estresado, mal usado o parcialmente fallando? En la práctica, la seguridad es corrección con un sistema de prioridades: algunas fallas son meramente molestas, otras pueden causar pérdidas financieras, violaciones de privacidad o daño físico.
Un bug es un defecto en el código o diseño. Un riesgo/hazardo es una situación que puede llevar a un resultado inaceptable. Un bug puede ser inocuo en un contexto y peligroso en otro.
Ejemplo: un off-by-one en una galería de fotos puede etiquetar mal una imagen; el mismo error en un calculador de dosis de medicación podría dañar a un paciente. El pensamiento de seguridad te obliga a conectar el comportamiento del código con consecuencias, no solo con el cumplimiento de la spec.
No necesitas métodos formales pesados para obtener beneficios inmediatos de seguridad. Los equipos pueden adoptar prácticas pequeñas y repetibles:
Estas técnicas encajan naturalmente con el razonamiento al estilo Hoare: haces explícitas las precondiciones (qué entradas son aceptables) y te aseguras de que las postcondiciones incluyan propiedades de seguridad (qué nunca debe ocurrir).
Las comprobaciones orientadas a seguridad tienen un coste—CPU, complejidad o rechazos falsos.
El pensamiento de seguridad va menos de demostrar elegancia y más de prevenir modos de fallo que no podemos permitir.
Las revisiones de código son donde el pensamiento de corrección rinde más rápido, porque puedes detectar suposiciones faltantes mucho antes de que los bugs lleguen a producción. El movimiento central de Hoare—declarar qué debe ser cierto antes y qué será cierto después—se traduce muy bien en preguntas de revisión.
Al leer un cambio, intenta enmarcar cada función clave como una pequeña promesa:
Un hábito sencillo del revisor: si no puedes decir las pre/post en una frase, probablemente el código necesita una estructura más clara.
Para funciones riesgosas o centrales, añade un pequeño comentario de contrato justo encima de la firma. Manténlo concreto: entradas, salidas, efectos secundarios y errores.
def withdraw(account, amount):
"""Contract:
Pre: amount is an integer > 0; account is active.
Post (success): returns new_balance; account.balance decreased by amount.
Post (failure): raises InsufficientFunds; account.balance unchanged.
"""
...
Estos comentarios no son pruebas formales, pero dan a los revisores algo preciso que comprobar.
Sé extra explícito cuando revises código que maneja:
Si el cambio toca alguno de estos puntos, pregúntate: “¿Dónde se imponen las precondiciones?” y “¿Qué garantías ofrecemos incluso cuando algo falla?”
El razonamiento formal no tiene por qué significar transformar toda tu base de código en un artículo matemático. La meta es gastar certeza adicional donde compense: lugares donde “parece bien en pruebas” no basta.
Encajan bien cuando tienes un módulo pequeño y crítico del que depende todo lo demás (autenticación, reglas de pago, permisos, interlocks de seguridad), o un algoritmo complejo donde errores off-by-one se esconden meses (parseadores, planificadores, cachés/evicción, primitivas de concurrencia, código tipo partición con muchos límites).
Una regla útil: si un bug puede causar daño real, pérdida financiera grande o corrupción de datos silenciosa, quieres más que revisión ordinaria + pruebas.
Puedes elegir entre “ligero” y “pesado”, y a menudo la mejor combinación viene al mezclar:
Decide el grado de formalidad sopesando:
En la práctica, también puedes tratar la “formalidad” como algo incremental: empieza con contratos explícitos e invariantes, y deja que la automatización te mantenga honesto. Para equipos que construyen rápido en Koder.ai—donde generar un front end React, un backend Go y un esquema Postgres puede ocurrir en un ciclo corto—snapshots/rollback y exportación del código facilitan iterar sin renunciar a contratos mediante pruebas y análisis estático en tu CI.
Usa esto como una puerta rápida “¿debemos formalizar más?” en planificación o revisión de código:
Lecturas recomendadas: design-by-contract, pruebas basadas en propiedades, model checking para máquinas de estado, analizadores estáticos para tu lenguaje e introducciones a asistentes de prueba y especificación formal.
La corrección significa que el programa satisface una especificación acordada: para cada entrada permitida y estado relevante del sistema, produce las salidas y efectos secundarios requeridos y maneja los errores según lo prometido. “Parece que funciona” normalmente significa que solo comprobaste unos pocos ejemplos, no todo el espacio de entradas ni las condiciones límite complicadas.
Los requisitos son el objetivo del negocio en lenguaje natural (por ejemplo, “ordenar la lista para mostrarla”). Una especificación es la promesa precisa y comprobable (por ejemplo, “devuelve una nueva lista ordenada ascendentemente, con la misma multiconjunto de elementos, y sin modificar la entrada”). La implementación es el código. Los errores suelen ocurrir cuando los equipos saltan directamente de requisitos a código sin escribir la promesa verificable.
Corrección parcial: si el código retorna, el resultado es correcto. Corrección total: el código retorna Y el resultado es correcto, es decir, la terminación también forma parte de la afirmación.
En la práctica, la corrección total importa siempre que “quedarse colgado” sea una falla visible para el usuario, un consumo injustificado de recursos o un riesgo para la seguridad.
Un triple de Hoare {P} C {Q} se lee como un contrato:
P (precondición): lo que debe ser cierto antes de ejecutar C.Las precondiciones son lo que el código necesita (por ejemplo: “los índices están en rango”, “los elementos son comparables”, “el lock está adquirido”). Si una precondición puede ser violada por los llamadores, o bien:
Si no, tus postcondiciones se convertirán en deseos en lugar de promesas comprobables.
Un invariante de bucle es una afirmación que es cierta antes de que comience el bucle, se mantiene cierta tras cada iteración y sigue siendo cierta cuando el bucle termina. Plantillas útiles:
0 <= i <= n)Si no puedes articular un invariante, es señal de que el bucle hace demasiadas cosas o los límites son confusos.
Normalmente nombras una medida (variant) que disminuye en cada iteración y no puede disminuir indefinidamente, por ejemplo:
n - i se reduce en 1Si no encuentras una medida decreciente, puede que exista un riesgo real de no-terminación (especialmente con duplicados o punteros estancados).
En Quicksort, la partición es la pequeña rutina de la que depende todo. Si la partición falla ligeramente, puedes obtener:
Por eso conviene declarar explícitamente el contrato de partición: qué debe cumplirse a la izquierda, a la derecha y que los elementos solo se reordenan (una permutación).
Los duplicados y el manejo de “igual al pivote” son puntos comunes de fallo. Reglas prácticas:
i/j se queden estancados)Si los duplicados son frecuentes, considera particionado de tres vías para reducir tanto errores como profundidad de recursión.
Las pruebas detectan errores concretos; el razonamiento puede eliminar clases enteras de errores (seguridad de índices, preservación de invariantes, terminación). Un flujo práctico híbrido es:
Para ordenación, dos propiedades de alto valor son:
C: el fragmento de código.Q (postcondición): lo que será cierto después de que C termine, asumiendo que P se cumplía.No hace falta escribir la notación en el código: usar la misma estructura en revisiones (“entradas que asumimos, salidas que garantizamos”) es la ganancia práctica.