Programación Imperativa

C APÍTULO 13

La Programación Imperativa
Índice del Capítulo
13.1. Introducción . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 213 13.2. Especificaciones de programas . . . . . . . . . . . . . . . . . . . . . . . . 213 13.2.1. Representación de variables iniciales y finales . . . . . . . . . . . . . 215 13.3. Leyes sobre tripletas . . . . . . . . . . . . . . . . . . . . . .. . . . . . . . 216 13.4. El transformador de predicados wp . . . . . . . . . . . . . . . . . . . . . 218 13.5. Ejercicios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 218

13.1. Introducción
A partir de ahora cambiaremos el modelo de computación subyacente, y por lo tanto el formalismo para expresar los programas. Esto no significa que lo hecho hasta ahora no nosserá útil en lo que sigue, ya que la experiencia adquirida en el cálculo de programas, y la consecuente habilidad para el manejo de fórmulas, seguirá siendo escencial en este caso, mostrando así que pese a sus diferencias, la programación funcional y la imperativa tienen varias cosas en común.

13.2. Especificaciones de programas
Los problemas que se presentan a un programador están, en general,expresados de manera informal, lo cual resulta demasiado impreciso a la hora de programar. Por eso es necesario precisar los problemas por medio de especificaciones formales. En la primera parte del curso se especificaba, usando lógica y un cálculo de funciones, el valor que debía calcularse. Este tipo de especificaciones era adecaudo para el desarrollo de programas funcionales. En el estilo deprogramación imperativa, la computación no se expresa como cálculo de valores sino como modificación de estados. Para desarrollar programas imperativos es por lo tanto deseable expresar las especificaciones como relaciones entre estados iniciales y finales. 213

214

13. L A P ROGRAMACIÓN I MPERATIVA

Así es que un programa en el modelo de la programación imperativa estará especificado mediante: • Unaprecondición: expresión booleana que describe los estados iniciales de las variables del programa, para los cuales se define el mismo. • Una postcondición: expresión booleana que describe los estados finales del programa luego de su ejecución. La notación que utilizaremos: {P } S {Q} donde P y Q son predicados y S es un programa (o secuencia de comandos), tiene la siguiente interpretación: Siempreque se ejecuta S comenzando en un estado que satisface P , el programa termina y el estado final satisface Q. P es llamada precondición de S, y Q su postcondición. La terna {P } S {Q} se denomina tripleta de Hoare. Derivar un programa imperativo consiste en encontrar S que satisfaga las especificación dada, es decir, consiste en encontrar S tal que, aplicado a un estado que satisfaga P , termine enun estado que satisfaga Q. Mientras que una verificación de que S es correcto (respecto a su especificación) consiste en probar que la tripleta {P } S {Q} es verdadera. Cuando querramos dar solo la especificación de un programa, no utilizaremos la tripleta {P } S {Q} , dado que esta notación no indica qué variables cambiaron en S. Por ejemplo, {true} S {x = y}, dice que S termina en un estado quesatisface x = y, pero no cuáles variables entre x e y cambiaron luego de la ejecución. Denotaremos formalmente una especificación como: {P } x :=? {Q} (13.1)

donde P es la precondición del programa, Q la postcondición, y x es la lista de variables que pueden cambiar de valor. En los lenguajes imperativos, también es necesario explicitar el tipo de las variables y constantes del programa, lo cual sehace a través de una declaración de variables y constantes. Esto completa la especificación del programa a la vez que indica implícitamente las operaciones que se pueden realizar con las variables y constantes declaradas. Como ejemplo consideremos la siguiente especificación de un programa que calcula el mayor múltiplo de 5 menor que n.

13.2. E SPECIFICACIONES

DE PROGRAMAS

215

|[...