Camilo Chacón Sartori - Computación y programación funcional

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} A 1; A 2; { ϕ 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 ϕ 1es la expresión lógica que se mantiene invariante antes y después de A 1; por otro lado, ϕ 2es 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:

• Boogie 8 : 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#).

• Why3 9 : 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.

• Coq 11 : es un sistema formal para realizar demostraciones matemáticas ( proofs en inglés) de algoritmos y teoremas.

Hemos incorporado en el apéndice Bun 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.

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, en primer lugar, en la tecnología a usar, agrega varias capas de dificultad para comprender el problema, ya que un lenguaje de programación trae consigo muchas cuestiones que no tienen nada que ver con la solución a un problema en sí, por ejemplo: cómo tratar con la memoria, la elección del tipo de datos o estructuras de datos, la refactorización, elegir correctamente el nombre de las variables, etc. Algunas de ellas, obviamente, son valiosas si queremos construir software de calidad y sostenible en el tiempo, pero no atacan al problema en cuestión. Todas esas cosas son parte de la implementación. En cambio, pensar en qué solucionar, de manera adecuada, lógicamente, es la labor de la etapa —olvidada y omitida— de especificación.

Debemos pensar antes de programar. Para esto se puede hacer uso de diferentes técnicas, algunas ya presentadas, como la verificación formal. O, en otros casos, podemos simplemente definir la solución a nuestro problema haciendo una demostración matemática que indique su comportamiento para cada argumento de entrada junto a su salida.

Leslie Lamport comenzaba diciendo su provocador artículo «If You’re Not Writing a Program, Don’t Use a Programming Language» («Si no estás escribiendo un programa, no uses un lenguaje de programación») lo siguiente: