Programación predictiva

Método de especificación de programas informáticos

Programación predicativa es el nombre original de un método formal para la especificación y refinamiento de programas , más recientemente llamado Teoría práctica de la programación, inventado por Eric Hehner . La idea central es que cada especificación es una expresión binaria ( booleana ) que es verdadera para los comportamientos aceptables de la computadora y falsa para los comportamientos inaceptables. De ello se deduce que el refinamiento es solo una implicación . Este es el método formal más simple y el más general, se aplica a programas secuenciales, paralelos, autónomos, comunicantes, terminantes, no terminantes, de tiempo natural, de tiempo real, deterministas y probabilísticos , e incluye límites de tiempo y espacio.

Los comandos en un lenguaje de programación se consideran un caso especial de especificación: aquellas especificaciones que son compilables. Por ejemplo, si las variables del programa son , , y , el comando := +1 es equivalente a la especificación (expresión binaria) = +1 ∧ = ∧ = en la que , , y representan los valores de las variables del programa antes de la asignación, y , , y representan los valores de las variables del programa después de la asignación. Si la especificación es > , demostramos fácilmente ( := +1) ⇒ ( > ), lo que dice que := +1 implica, o refina, o implementa > . ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle z}$ ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle x'}$ ${\displaystyle y}$ ${\displaystyle y'}$ ${\displaystyle y}$ ${\displaystyle z'}$ ${\displaystyle z}$ ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle z}$ ${\displaystyle x'}$ ${\displaystyle y'}$ ${\displaystyle z'}$ ${\displaystyle x'}$ ${\displaystyle y}$ ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle x'}$ ${\displaystyle y}$ ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle x'}$ ${\displaystyle y}$

Las pruebas de bucles se simplifican enormemente. Por ejemplo, si es una variable entera, para demostrar que ${\displaystyle x}$

mientras >0 hacer := –1 od ${\displaystyle x}$ ${\displaystyle x}$ ${\displaystyle x}$

refina o implementa la especificación ≥0 ⇒ =0, prueba ${\displaystyle x}$ ${\displaystyle x'}$

si >0 entonces := –1; ( ≥0 ⇒ =0) de lo contrario fi ⇒ ( ≥0 ⇒ =0) ${\displaystyle x}$ ${\displaystyle x}$ ${\displaystyle x}$ ${\displaystyle x}$ ${\displaystyle x'}$ ${\displaystyle ok}$ ${\displaystyle x}$ ${\displaystyle x'}$

donde = ( = ) es el comando vacío o que no hace nada. No hay necesidad de un bucle invariante o de un punto mínimo fijo . Los bucles con múltiples salidas intermedias superficiales y profundas funcionan de la misma manera. Esta forma simplificada de prueba es posible porque los comandos y las especificaciones del programa se pueden mezclar de manera significativa. ${\displaystyle ok}$ ${\displaystyle x'}$ ${\displaystyle x}$

El tiempo de ejecución (límites superiores, límites inferiores, tiempo exacto) se puede demostrar de la misma manera, simplemente introduciendo una variable de tiempo. Para demostrar la terminación, demuestre que el tiempo de ejecución es finito. Para demostrar la no terminación, demuestre que el tiempo de ejecución es infinito. Por ejemplo, si la variable de tiempo es , y el tiempo se mide contando iteraciones, entonces para demostrar que la ejecución del bucle while anterior toma tiempo cuando es inicialmente no negativo, y toma una eternidad cuando es inicialmente negativo, demuestre ${\displaystyle t}$ ${\displaystyle x}$ ${\displaystyle x}$ ${\displaystyle x}$

si >0 entonces := –1; := +1; ( ≥0 ⇒ = + ) ∧ ( <0 ⇒ =∞) de lo contrario fi ⇒ ( ≥0 ⇒ = + ) ∧ ( <0 ⇒ =∞) ${\displaystyle x}$ ${\displaystyle x}$ ${\displaystyle x}$ ${\displaystyle t}$ ${\displaystyle t}$ ${\displaystyle x}$ ${\displaystyle t'}$ ${\displaystyle t}$ ${\displaystyle x}$ ${\displaystyle x}$ ${\displaystyle t'}$ ${\displaystyle ok}$ ${\displaystyle x}$ ${\displaystyle t'}$ ${\displaystyle t}$ ${\displaystyle x}$ ${\displaystyle x}$ ${\displaystyle t'}$

donde = ( = ∧ = ). ${\displaystyle ok}$ ${\displaystyle x'}$ ${\displaystyle x}$ ${\displaystyle t'}$ ${\displaystyle t}$

Referencias

• ECR Hehner, a Practical Theory of Programming , Springer-Verlag 1993. Edición más reciente en línea en a Practical Theory of Programming.

Enlaces externos

• Publicaciones de Eric Hehner .