Читать книгу Computación y programación funcional - Camilo Chacón Sartori - Страница 21

Dentro de la computación tenemos la ingeniería de software, que es un área particularmente relacionada con el ciclo de vida de un producto, la gestión de personas, la metodología de desarrollo, la planificación y el diseño de pruebas, entre otras labores. Y dentro de la misma tenemos la verificación de software, la cual es una disciplina dividida en dos categorías: estática y dinámica.

La verificación formal es parte de la estática, y la dinámica está relacionada al conocido proceso de testing para encontrar errores (bugs en inglés) en un software (aunque esta última se podría ver más como una «validación» que una verificación).

La verificación formal es un área que trata sobre la correctitud de un algoritmo; es decir, hace referencia a si un algoritmo cumple o no con su especificación. Un algoritmo es correcto si cumple lo siguiente: (1) hace lo que dice la especificación; (2) los valores de entrada generan los valores «correctos» de salida, y (3) se ejecuta en un tiempo finito (es decir, evita caer en el problema de la parada [se refiere a que no se puede determinar si un algoritmo entrará en un ciclo infinito que nunca terminaría de ejecutarse]).

Esta área fue introducida por Robert W. Floyd en su artículo «Assigning Meanings to Programs» («Asignar significados a los programas»). Por medio de aserciones lógicas se comprueba la validez de un algoritmo haciendo uso de pruebas de correctitud, equivalencia y terminación. El mismo autor menciona en dicho artículo: «este documento intenta proporcionar una base adecuada para las definiciones formales de los significados de los programas en los lenguajes de programación apropiadamente definidos.».

Cada instrucción de un algoritmo es comprobada a través de expresiones lógicas (aserciones). Es decir, podemos comprobar la validez de un algoritmo en el ámbito de la especificación sin necesidad de ejecutarlo para saber si devolverá el valor correcto. Es por esto que se trata de una verificación estática.

Por su mismo mecanismo, la verificación formal es más compleja de realizar que el testing, ya que se debe pensar y analizar exhaustivamente cómo trabajará cada algoritmo, a través de un conjunto de aserciones bien definidas, desde los argumentos de entrada hasta los de salida. Una técnica formal que nos ayuda a trabajar con esto es la llamada lógica de Hoare.

Lógica de Hoare

Tony Hoare, en su artículo «An Axiomatic Basis for Computer Programming» («Una base axiomática para la programación computacional»), introdujo un sistema formal con un conjunto de reglas lógicas aplicadas sobre declaraciones en un lenguaje determinado para verificar la correctitud de un algoritmo (se le conoce como lógica de Hoare o lógica de Floyd-Hoare).

Básicamente es una forma de axiomatizar un algoritmo. Se le dice «Hoare Triple» a la fórmula {ϕ₁} A {ϕ₂}, donde A es un algoritmo definido en algún lenguaje formal imperativo, ϕ₁ es una precondición y ϕ₂ una poscondición. (En la literatura se usa la palabra «program» [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: {ϕ₁} A₁; A₂; {ϕ₃}. 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»⁷, es decir, si su estado se mantiene igual antes y después del ciclo.

Esta regla quiere decir que ϕ₁ es la expresión lógica que se mantiene invariante antes y después de A₁; por otro lado, ϕ₂ 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 ϕ₂, 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⁸: 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⁹: 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+¹⁰: 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¹¹: 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.