Verificación formal de algoritmos
Podemos entender un algoritmo como una caja negra que toma como entrada un conjunto de datos, los procesa y que genera alguna salida función de dicha entrada. En una primera etapa para la construcción de un algoritmo se lleva a cabo un diseño y una especificación del problema a resolver, que comprende las entradas, salidas y procesos necesarios para resolver el problema en cuestión. Seguidamente, se construye un algoritmo en base a esta especificación.

Es de importancia verificar si el algoritmo construido resuelve efectivamente el problema planteado o si requiere modificaciones. Una manera de llevar a cabo la verificación de un algoritmo es eligiendo un lote de datos de prueba, ejecutar el algoritmo y observar los resultados. De producirse un error, se procede a la depuración del algoritmo y a la introducción de las modificaciones necesarias para salvar dicho error. Pero, ¿como podemos asegurarnos que hemos probado todas las posibles entradas para las cuales se puede producir un error? En problemas sencillos quizás podemos hacer pruebas exhaustivas y asegurarnos de que el algoritmo es correcto, pero la realidad es que esto no es viable para problemas cuyo dominio es muy grande (o infinito). Por suerte, algunos matemáticos muy inteligentes encontraron una manera de verificar formalmente que un algoritmo es correcto.
La verificación formal de algoritmos es una técnica (basada en Lógica de Primer Orden y en la Lógica de Hoare) para demostrar la correctitud de un algoritmo previo a su ejecución. Decimos que esta es una validación a priori de la correctitud del mismo, ya que no es necesario llegar a la ejecución del mismo para probar esto.
Especificación formal de algoritmos
Para llevar a cabo la verificación formal de un algoritmo, primero es necesario expresar a este en un algún lenguaje o notación formal. Para ello, representaremos un algoritmo con lo que se conoce como una tripla de Hoare. Una tripla de Hoare tiene la forma {P} C {Q}, donde P y Q son aserciones sobre las entradas y las salidas, respectivamente, y C es un comando o instrucción de nuestro algoritmo que transforma las entradas en las salidas especificadas. Las aserciones son predicados lógicos que explicitan las condiciones que han de cumplir los datos de entrada y de salida, de tal manera que si la aserción P es cierta, entonces la ejecución de C nos llevará a que Q sea también verdadera, y por lo tanto nuestro algoritmo correcto.
Sobre las aserciones
Estableceremos unas reglas generales relativas a las aserciones que serán de utilidad para verificar nuestros algoritmos. Estas reglas provienen del sistema formal de Hoare, un sistema de reglas de inferencia para razonar sobre algoritmos.
Dadas dos aserciones R y S, diremos que R es más fuerte que S si R implica S (R ⇒ S). Luego, diremos que S es más débil que R. Que R sea más fuerte que R es como decir que es más restrictivo en cuanto a las condiciones que aplica sobre las variables que en ella intervienen. O sea, el conjunto de estados que satisfacen R es un subconjunto de aquellos que satisfacen S. Por ejemplo, la aserción {i > 1} es más fuerte que {i > 0}, dado que los valores de i que satisfacen la primera satisfacen también la segunda.
Verificación formal hacia atrás
De manera conceptual, todo el proceso de verificación se basa en encontrar la Precondición Más Débil o PMD (en inglés Weakest Precondition o WP), es decir, la precondición más débil para la cual, luego de ejecutar C, Q será verdadera. Es decir, para la especificación formal de nuestro algoritmo {P} C {Q}, trataremos de encontrar PMD tal que {PMD} C {Q} sea correcto por construcción. Luego, si P ⇒ PMD, entonces habremos verificado que {P} C {Q} es correcto.
Para encontrar PMD utilizaremos un enfoque hacía atrás: a partir de Q y dependiendo de las sentencias de C, aplicaremos una serie de reglas generales hasta llegar a PMD.
Regla para instrucciones de asignación
Las instrucciones de asignación poseen la forma V = E, donde V es una variable y E es un valor o una expresión. Si tenemos una tripla {P} V = E {Q}, entonces podemos hallar PMD sustituyendo todas las ocurrencias de V por E que encontremos en Q. Luego, si P ⇒ PMD, entonces {P} V = E {Q} será correcto.
Q: Determinar PMD para que {PMD} y = x² {y > 1} sea correcto.
R: Aplicando la regla vista anteriormente, reemplazamos en Q las ocurrencias de y por x². Entonces PMD = (x2 > 1) ⇒ {(x > 1) 🇻 (x < -1)}. Luego {(x > 1) 🇻 (x < -1)} y = x2 {y > 1 } es correcto.
Regla para instrucciones secuenciales
Esta regla se aplica para instrucciones concatenadas. Por instrucciones concatenadas nos referimos a aquellas que se ejecutan de manera secuencial, donde el estado final de una instrucción se convierte en el estado inicial de la siguiente.
La regla nos dice que si C1 y C2 son dos partes de un código, y siendo C1;C2 la concatenación de ellas, entonces si {P} C1 {R} y {R} C2 {Q} son dos triplas de Hoare correctas, entonces {P} C1;C2 {Q} es también correcta. La forma en que aplicaremos esta regla será primero encontrar la precondición más débil R tal que {R} C2 {Q} sea correcta. Luego, R será la postcondición que usaremos para encontrar PMD para que {PMD} C1 {R} sea correcta. Finalmente, afirmamos que {P} C1;C2 {Q} es correcta si P ⇒ PMD.
Q: Demostrar que {T} c=a+b; c=c/2 {c==(a+b)/2} es correcto. Considerar T como el predicado tautológico.
R: En primera instancia encontramos R tal que {R} c=c/2 {c==(a+b)/2} es correcto. Utilizando la regla para asignaciones reemplazamos en {c==(a+b)/2} las ocurrencias de c por c/2. Luego R = {c/2 == (a+b)/2} = {c == a+b}. Seguidamente, tomamos R como postcondición para encontrar PMD tal que {PMD} c = a+b {R}. Luego PMD = {a + b == a + b} = {T}, y como {T} ⇒ {T}, entonces {T} c=a+b; c=c/2 {c==(a+b)/2} es correcto.
Regla para instrucciones de selección
Para demostrar la correctitud de partes de un algoritmo que involucran instrucciones de selección de la forma if-then-else, consideraremos las partes fundamentales de estas estructuras. Toda instrucción de selección posee una condición B que será evaluada. Si B es verdadera, entonces se ejecutará una parte de código C1. Opcionalmente, si B es falsa se ejecutará una porción de código C2.

Si deseamos probar que una instrucción de este tipo es correcta, debemos probar que las siguientes ternas son correctas de manera simultánea:
- Si el estado inicial satisface B además de P, se ejecutará C1. Luego es necesario probar que {P ∧ B} C1 {Q} es correcto
- Si el estado inicial no satisface B se ejecutará C2. Luego es necesario probar que {P ∧ ㄱB} C2 {Q} es correcto.
Luego, se debe probar la veracidad de:
{P ∧ B} ⇒ PMD(C1, Q) ∧ {P ∧ ㄱB} ⇒ PMD(C2, Q)
Q: Demostrar que {T} if (a >b) then m=a else m = b{(m ≥a)∧(m ≥b)} es correcto.
R: En primera instancia probaremos que {a>b} m=a {(m ≥a)∧(m ≥b)} es correcta. Usando la regla para asignación reemplazamos en {(m ≥a)∧(m ≥b)} las ocurrencias de m por a. Luego PMD(m=a, {(m ≥a)∧(m ≥b)}) = {(a ≥a)∧(a ≥b)} = {a ≥b}. Luego, vemos que {a>b}⇒{a ≥b} y entonces la parte if-then de la instrucción es correcta
Seguidamente, debemos probar que {ㄱ(a>b)} m=b {(m ≥a)∧(m ≥b)} es correcta. Nuevamente, usamos la regla para asignaciones y tenemos que PMD(a ≤ b, {(m ≥a)∧(m ≥b)}) = {(b ≥a)∧(b ≥b)} = {b ≥a}. Luego, vemos que {b ≥a}⇒{a ≤ b} y entonces la parte elsede la instrucción es correcta y por lo tanto toda la instrucción lo es.
Conclusión
Hemos visto que existen técnicas para probar que un algoritmo que hemos construido es correcto previo a ejecutarlo. Esto nos puede ahorrar tiempo y hacernos quedar como unos verdaderos nerds frente a nuestros colegas.
Si te resulto de interés o de ayuda el artículo, déjame un comentario y así consideraré hacer una segunda parte que contemple las reglas para probar que instrucciones de bucle (for, while, etc) son correctas.