[que vendría siendo un programa computacional] en vez de «algoritmo», dado que se enfoca más en un conjunto de estos últimos; en nuestro caso, para simplificar esto, usaremos solamente «algoritmo».)
Por ejemplo, podemos crear la gramática de un simple lenguaje imperativo utilizando la notación EBNF (esta la veremos en detalle en el capítulo 4):
Así, esta gramática puede soportar, por ejemplo, los siguientes códigos fuente:
A continuación, veamos cuatro ejemplos —bastante triviales pero instructivos— donde podemos verificar un posible defecto en un algoritmo escrito en este lenguaje usando la lógica de Hoare:
1. {x > 0} x := * 2; {x ≥ 2}
2. {x == y – 1} x := x + 1; y := y + 2; {x == y}
3. {x == y == z} x := y + 1; z := x + 1; {(x > y) < z}
4. {(x > y) ∧ (x ≥ 0) ∧ (y > 0)}
if x > 0 begin
x := y – 1;
else
x := y * –2;
end
{x < y}
Cada uno de los ejemplos anteriores es válido. Siempre que la precondición sea verdadera, la poscondición debe cumplirse; en caso contrario, tenemos un error en nuestro algoritmo. Por ejemplo, si vemos el caso de (1), si reemplazamos por cualquier número mayor a 0, el valor de x después de la ejecución del algoritmo debe ser mayor o igual a 2. Y, dado que el algoritmo incrementa x por su doble, esto siempre será verdadero. Lo mismo ocurre en los ejemplos siguientes. En caso contrario, si la precondición o la poscondición no se cumplen, entonces el algoritmo no concreta la verificación y, por tanto, no es válido. Entonces, si se le asigna el valor 0 a x en (1), este no sería válido porque no puede cumplir con la primera precondición: x > 0.
La lógica de Hoare nos permite pensar en las condiciones exactas de los valores de entrada y salida. O sea, podemos definir correctamente el estado previo y posterior a la ejecución del algoritmo. ¿Cómo? Usando reglas. Conozcamos algunas de ellas:
Regla de composición. Utiliza reglas de inferencias, que tienen la siguiente estructura:
Si tenemos dos axiomas en la parte superior,
podemos inferir la siguiente regla: {ϕ1} A1; A2; {ϕ3}. Esto quiere decir que, si las instrucciones superiores son verdaderas por inferencia, las inferiores también lo serán.
Por ejemplo, las siguientes instrucciones cumplen esta regla:
Regla de iteraciones. La podemos usar cuando necesitamos comprobar la correctitud de un algoritmo que usa ciclos o bucles (por ejemplo, while).
Nos permite comprobar si una variable se mantiene «invariante»7, es decir, si su estado se mantiene igual antes y después del ciclo.
Esta regla quiere decir que ϕ1 es la expresión lógica que se mantiene invariante antes y después de A1; por otro lado, ϕ2 es la expresión que permite terminar el while (evitando así un bucle infinito).
Un ejemplo de esta regla es el siguiente:
En el ejemplo superior, vemos que el axioma (x > 0 ∧ x < 10) es ϕ2, y dado aquello, se evaluará en el while hasta que x sea igual o superior a 10. Por tanto, la variable se irá incrementando, pero seguirá siendo invariante a la expresión y < 10.
Herramientas para la verificación formal
Es posible aplicar estas técnicas a ambientes productivos. Las siguientes herramientas permiten realizar verificación formal en distintos lenguajes de programación:
• Boogie8: es un lenguaje de verificación formal intermedio. Permite utilizar otros lenguajes diseñados para la verificación (por ejemplo, Havoc para C y Spec# para C#).
• Why39: es una plataforma para verificación de software. Provee un lenguaje llamado Why3ML que también puede servir como intermediario de otros lenguajes de verificación.
No obstante, también existen los lenguajes de especificación que están diseñados puramente para la verificación formal. No son lenguajes de programación. Estos tienen la ventaja de omitir detalles innecesarios que contienen los lenguajes de programación para, en cambio, centrarse en algo importante: pensar en un alto nivel el diseño de un software. Dos de los más relevantes están a continuación:
• TLA+10: es un pequeño lenguaje de verificación formal similar a las matemáticas. Especialmente utilizado para algoritmos distribuidos y concurrentes. Según el mismo sitio web «it’s the software equivalent of a blueprint» («es el equivalente a un plano en el software»). Su creador fue Leslie Lamport.
• Coq11: es un sistema formal para realizar demostraciones matemáticas (proofs en inglés) de algoritmos y teoremas.
Hemos incorporado en el apéndice B un pequeño tutorial de TLA+ que es, en cierta medida, nuestro lenguaje de especificación preferido. Por su sencillez y elegancia para expresar operaciones matemáticas y por aplicar el concepto de «invariancia inductiva», cuyo significado puede descubrir en dicho apartado.
En consecuencia, la verificación formal aspira a pensar cómo debe funcionar un algoritmo y no, simplemente, seguir una estrategia de prueba y error. Persigue el siguiente lema: debemos pensar antes de programar.
2.2.2 ¿Pensar antes de programar?
La especificación tiene como objetivo «pensar antes de programar». Esto hace hincapié en que, si no se piensa ni se analiza en detalle el problema X a solucionar, solo nos estamos embarcando en una lucha para entender una tecnología Y sin comprender el problema X. La importancia del qué sobre el cómo. Esto forma fanáticos de la herramienta, no así de resolver problemas.
Pensar,