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

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


Скачать книгу
[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):

Illustration

      Así, esta gramática puede soportar, por ejemplo, los siguientes códigos fuente:

Illustration

      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:

Illustration

      Si tenemos dos axiomas en la parte superior,

Illustration

      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:

Illustration

      Regla de iteraciones. La podemos usar cuando necesitamos comprobar la correctitud de un algoritmo que usa ciclos o bucles (por ejemplo, while).

Illustration

      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:

Illustration

      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:

      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:

      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,


Скачать книгу