UNED

Se inicia aquí el tratamiento de las técnicas de especificación de programas. Las técnicas de especificación se tratan en el Capítulo 2 de Peña y se incluyen en ese capítulo numerosos ejemplos que conviene repasar. Resulta también aconsejable repasar el capítulo 1 de otro de los textos recomendados:

JL.Balcázar. "Programación Metódica". McGraw-Hill. 1993

Este capítulo contiene una descripción simple y rigurosa de los conceptos básicos de especificación. La nota adicional ("excursión" en el texto) sobre el transformador de predicados pmd (precondición más débil) resulta también muy interesante.

Ese material cubre de forma apropiada el tema. En estos artículos se tratarán de aclarar conceptos de manera, a veces, informal, con ejemplos e incidiendo en los puntos que suelen generar dudas y en las aplicaciones al diseño y verificación de algoritmos. 

Introducción

En los artículos que P.J. Plauger (relevante miembro de los comités ANSI encargados de la normalización del lenguaje C, y luego de C++) publicaba en la revista "The C User's Journal" , y en los que explicaba la evolución del proceso de normalización, era frecuente el encontrarse con apartados análogos al siguiente (traducción libre del artículo original):

"Algunas de las funciones declaradas en el módulo de biblioteca <string.h>¹ toman un argumento de longitud, que puede ser cero. Se debatió qué ocurre cuando ese argumento es cero, resultado:

Añadido a la subclaúsula 7.11.1, página 162 ² :

Cuando un argumento declarado como size_t n determina la longitud del vector para la función, n puede tomar el valor cero en una llamada a la función ........... En tal llamada la función que copia caracteres deberá copiar cero caracteres, mientras que la función que compara dos secuencias de caracteres deberá devolver cero. "

P. J. Plauger. "The C Users Journal", Enero 1994

¹ El módulo <string.h> de la biblioteca C estándar es el contiene las funciones que permiten copiar, comparar, ... secuencias de caracteres ("strings")

² Del documento ANSI normalizador del lenguaje C y biblioteca estándar

Este tipo de decisiones sobre ambigüedades en la definición del lenguaje o en sus funciones de biblioteca estándar eran frecuentes en el comité de normalización de C, según reflejaban Plauger, y otros, en sus artículos. En algunos casos se daban discusiones filosóficas del tipo: " ¿ Es posible definir vectores de dimensión cero ? ", " Es posible reservar memoria dinámica de tamaño cero, si es así, ¿ a qué apuntará el puntero resultante ?" . 

Sin necesidad de recurrir a entornos de trabajo como el presentado (comité normalizador) estos problemas de ambigüedad se presentan cuando, simplemente, un equipo de programadores ha de intercambiar módulos entre sí. Muchas veces, la única forma de saber a ciencia cierta que hace un procedimiento o función es revisar su propia implementación, rompiendo así un principio básico en programación: la separación nítida entre QUÉ hace un procedimiento y CÓMO lo hace. El usuario del procedimiento no debería verse afectado ante cambios en el CÓMO si se mantiene constante el QUÉ. Este es uno de los principios básicos de programación estructurada y una de las características fundamentales de la moderna programación orientada a objetos (Encapsulación).

Un ejemplo puede ser el de cualquiera de los contenedores de objetos clásicos. Por ejemplo la PILA. El usuario sólo debe conocer qué objetos se pueden "apilar" y disponer de funciones para crear una nueva pila, "apilar", "desapilar" y quizás comprobar si "pila vacía" o "pila llena". El implementador ha podido implementar la pila inicialmente por medio de un vector estático de objetos de tamaño fijo. Posteriormente decide cambiar a una implementación basada en una lista dinámica, por ejemplo. El usuario no debería verse afectado ante ese cambio si la interfase no cambia. Esta sería, por ejemplo, la declaración de los procedimientos de un ejemplo en MODULA 2 en el que utiliza una pila para almacenar los distintos ensayos pendientes de realizar en un algoritmo de juego:

PROCEDURE NuevaPila(VAR InicioDePila:PPila);



PROCEDURE Empilar(VAR InicioDePila: PPila;Nuevo: Ensayo);



PROCEDURE Desapilar(VAR InicioDePila:PPila;VAR e: Ensayo);



PROCEDURE PilaVacia(VAR InicioDePila:PPila): BOOLEAN;

El implementador ha podido utilizar un vector para desarrollar la pila o una lista dinámica u otro tipo de implementación. El utilizador solo ve el objeto abstracto "Pila de Ensayos".

Las técnicas de especificación pretenden resolver las ambigüedades al establecer QUÉ hace un segmento más o menos extenso de programa (puede ser desde una sola instrucción a todo un procedimiento o función o todo un programa). Es importante, también, indicar cuales son los requisitos previos para que el segmento de programa obtenga el resultado indicado. Esta es la técnica conocida como especificación Pre-Post.

Pero, en la etapa de desarrollo, es necesario mezclar el CÓMO con el QUÉ. En concreto se tienen dos tipos de problemas:

a) El problema de verificación

Una vez establecido el QUÉ debe hacer un algoritmo, verificar que el CÓMO conduce a los resultados establecidos en el QUÉ.

b) El problema de diseño

Obtener una implementación (es decir un CÓMO) que haga lo establecido en el QUÉ.

Estado de un programa

Un programa de computador evoluciona a lo largo de su ejecución entre distintos estados. Un estado queda definido al establecer los valores que adquieren todas las estructuras de datos involucradas en el programa.

Cualquier segmento de programa o algoritmo que sea útil tratará de cambiar el estado de ciertas variables relevantes desde una situación inicial menos concreta a otra más concreta y elaborada.

Una vez establecidas las variables relevantes en el problema, el conjunto de estados posible viene dado por las combinaciones de valores en que pueden encontrarse esas variables. Imagínese, por ejemplo, que el programa que controla el desplazamiento de un ascensor utiliza dos variables relevantes:

p: indica su posición como valor del piso inferior más próximo a la localización del ascensor.

m. indica el estado de marcha y puede tomar tres valores: REPOSO, SUBIENDO, BAJANDO.

Los posibles estados son, en este caso, enumerables con relativa facilidad. Así si existen 4 pisos: Bajo, 1º, 2º, 3º se tendrán los estados posibles:

{Bajo, REPOSO}, {Bajo, SUBIENDO}, {Bajo, BAJANDO},{1º, REPOSO}...

... {4º, REPOSO}, {4º BAJANDO}

En este problema los estados son enumerables, pero a poca complejidad que tenga un programa, la enumeración no es posible. 

Una técnica que permite establecer de forma más compacta los posibles estados que ha alcanzado un programa en un momento dado es el establecimiento de un Predicado, Aserto o Aserción sobre las variables involucradas en el problema. Así, si se está en el 2º piso y lo que interesa es saber si el ascensor sube desde un piso inferior se puede decir que:

"El ascensor hacia el 2º piso sube desde un piso inferior" equivale a que :

" p < 2º Y m= SUBIENDO" 

Obsérvese que este Predicado lógico (o Aserto ó Aserción) sólo puede tener dos soluciones: Cierto o Falso. Cuando toma el valor Cierto queda determinado un subconjunto de estados : {{Bajo, SUBIENDO}, {1º, SUBIENDO}}. Es importante mantener esa visión dual entre Predicado y subconjunto de estados que determina.

Predicados, Asertos o Aserciones

Como se ha indicado en el apartado anterior un Predicado (o Aserto) es una expresión , cuyo resultado es de tipo booleano (Falso o Cierto), que puede incorporarse a texto del programa como comentario, y que pretende establecer las condiciones que ha de cumplir el ESTADO del programa en ese punto para que se considere correcta su evolución hasta el punto indicado. En los Predicados se pueden utilizar operaciones de cualquier tipo, sin necesidad de que estén soportadas por el lenguaje de programación, siempre que sean conocidas por los que lean dichos predicados y estén establecidas sin ambigüedad. Así en un programa de CAD (diseño asistido por ordenador), dado un círculo (normalmente definido por las coordenadas del centro y el radio) y un cuadrado (definido, por ejemplo, por las coordenadas de su extremo superior izquierdo y por su lado) se puede establecer en un punto de un programa el aserto (suponiendo como variables relevantes el círculo Circulo1 y el cuadrado Cuadrado1):

(* El cuadrado Cuadrado1 está inscrito en el círculo Circulo1 *) (Predicado 1)

Desde luego el lenguaje de programación que se utilice no tiene por qué soportar la operación que permite inscribir un cuadrado en un círculo. Si será necesario que cualquiera que lea el programa tenga claro el concepto de polígono inscrito en un círculo. Este concepto habrá de haberse definido sin ambigüedad antes, o se supondrá conocido por geometría elemental. El predicado anterior, colocado en un punto dado del programa de CAD, tiene como objeto establecer una condición que debe ser cierta en dicho punto para que las operaciones que se realicen a continuación conduzcan al resultado deseado. Por ejemplo, si en la variable Radio1 se almacena el radio de Circulo1 y se tiene una variable Diagonal genérica, tras la instrucción:

Diagonal := 2* Radio1;

se cumplirá con seguridad:

(* La variable Diagonal contiene el valor de la diagonal de Cuadrado1 *)

si antes de ejecutar la instrucción era cierto el Predicado 1.

Es decir, el hecho de que en un punto dado del programa se cumpla una condición dada permite, que tras una nueva instrucción, sea posible determinar si se cumple otra condición. Esta técnica de avance por las condiciones que cumplen las variables del programa (sus distintos estados) es la que ha de seguirse en el diseño y verificación de algoritmos.

En la búsqueda de la economía de expresión y la eliminación de ambigüedades, en la medida de lo posible, es conveniente establecer un lenguaje distinto al natural para la escritura de predicados lógicos. Este lenguaje se establece en la bibliografía recomendada y se seguirá en estos apuntes. En lo que sigue los predicados se incluirán entre llaves {} en lugar de entre limitadores de comentario de MODULA-2 y se empezarán a utilizar los operadores lógicos elementales: Ù ( Y lógico) y Ú (O lógico)

Predicados y problema de verificación

Supóngase que se tiene el siguiente programa, que incluye un predicado previo (precondición) y otro posterior (postcondición) y en el que intervienen cuatro variables relevantes: x, y, u y v. definidas como de tipo real:

{ x>0 Ù y>0 }

 u:= x*y;

 v:= u/x;

 u:= u/y;

{ u=x Ù v=y }

El primer predicado indica que se asegura que las variables involucradas en el problema tendrán valor positivo al inicio del segmento de programa. El segundo predicado indica que, tras las operaciones, u tiene el valor original de x y v el valor original de y. Se ha de verificar si esto es cierto, suponiendo cierta la condición inicial (precondición). La verificación de este algoritmo se realiza sucesivamente partiendo del último predicado (postcondición)

si tras la instrucción u:= u/y se tiene u=x Ù v=y antes de esa instrucción ha de ser 

{ u=x*y Ù v=y Ù y ¹ 0 }

la condición para u se obtiene fácilmente si, en base a la condición final u=x ,se sustituye en la operación u por x, se tiene x=u/y de donde se tendrá que u ha de ser igual a x*y, y ha de ser distinto de cero para que la división tenga sentido.

si tras la instrucción v:= u/x ha de tenerse que:

{ u=x*y Ù v=y Ù y ¹ 0 }

se deberá tener antes que y=u/x, lo que conduce de nuevo a u=x*y, y además que y=x*y/x, lo que conduce a que y=y, lo cual es evidentemente cierto. Además para que y sea distinto de cero tras esa instrucción, antes ha de ser u distinto de cero y x distinto de cero. Por tanto, la condición que debe cumplirse antes de la instrucción v:=u/x será :

{ u=x*y Ù y ¹ 0 Ù x ¹ 0 }

para que tras la instrucción u:= x*y se cumpla {u=x*y} no es, en principio, necesaria ninguna condición previa, ya que la operación asegura ese resultado, por tanto la condición exigible para la corrección del programa es que en ese punto sea cierto el predicado:

{ y ¹ 0 Ù x ¹ 0 }

El predicado que indica las condiciones de las variables en ese punto es el inicial (precondición) que dice que tanto x como y son mayores que cero. Estas condiciones garantizan las mínimas necesarias para la corrección del algoritmo, que x e y sean distintas de cero. Luego el algoritmo es correcto, en principio.

Obsérvese el criterio para determinar la corrección: se han recorrido en orden inverso las operaciones determinando la condición previa a cada una de ellas para que tras su ejecución se cumpla la condición posterior, así se llega a una condición inicial mínima que han de cumplir las variables: ambas han de ser no nulas. En ese punto se nos indicaba que ambas eran estrictamente mayores que cero, como esta condición asegura que, desde luego, ambas son no nulas, la condición mínima exigible queda asegurada y el algoritmo es correcto. 

No se ha tenido en cuenta un detalle: en la operación u=x*y no se ha de producir un desbordamiento en la multiplicación. Esta es una condición denominada de dominio y se ha de prestar también cuidado a este tipo de condiciones en los programas reales. 

La condición mínima exigible al inicio del algoritmo es la que J.L Balcázar denomina Precondición Mas Débil (pmd). El algoritmo será correcto si el predicado establecido al inicio en la especificación es más fuerte que la pmd. (El concepto de predicado más fuerte que otro se establecerá en un apartado posterior, en principio simplemente decir que un predicado más fuerte "exige" más a las variables).

Predicados y problema de diseño 

El diseño de algoritmos pretende encontrar las operaciones que conducen a un estado deseado partiendo de un estado inicial previo. Este estado inicial ha de ser razonablemente fácil de establecer previamente o, en otras palabras, el estado final ha de ser mucho más elaborado que el inicial, para que el algoritmo haga una función verdaderamente útil. Por tanto, en el diseño se establecen operaciones de forma que la condición final se vaya alcanzando sucesivamente a partir de condiciones menos fuertes. 

Supóngase que se nos pide el diseño de un algoritmo capaz de encontrar el índice correspondiente al mayor entre los elementos de un vector de enteros de tamaño 3 y con índices 1..3. Es decir se pide que, dado el vector v[1..3] de enteros, en una variable p se obtenga un valor tal que:

 {1<= p<=3 Ù v[p] ³ v[1] Ù v[p] ³ v[2] Ù v[p] ³ v[3]}

Para obtener este resultado se irán añadiendo instrucciones de forma que la condición previa a cada una de ellas sea más débil que la posterior, así si se hace:

 si v[3]>v[p] entonces p:=3;     (I1)

se tendrá que antes de esta instrucción sólo será necesario que

 { 1<= p<=3 Ù v[p] ³ v[1] Ù  v[p] ³ v[2]}

ya que la instrucción asegura que v[p] ³ v[3], si antes de la instrucción I1 se hace

 si v[2]>v[p] entonces p:=2;     (I2)

se tendrá que para que tras esa instrucción se cumpla (P2) tan sólo será necesario que antes se cumpla

 {1<=p<=3Ù v[p] ³ v[1]}

si antes de la instrucción I2 se hace

 si v[1]>v[p] entonces p:=1;     (I3)

entonces antes de esa instrucción tan sólo será necesario que 

 {1<=p<=3}

Esta condición se cumple fácilmente si se hace p:=1, por ejemplo. Es decir el programa resultante es (se incluyen los predicados intermedios como comentario):

 {cierto}

 p:=1;

 {1<= p<=3 }

 si v[1]>v[p] entonces p:=1;     (I3)

 {1<=p<=3 Ù v[p] ³ v[1]}

 si v[2]>v[p] entonces p:=2;     (I2)

 {1<= p<=3 Ù v[p] ³ v[1] Ù v[p] ³ v[2]}

 si v[3]>v[p] entonces p:=3;     (I1)

 {1<=p<=3 Ù v[p] ³ v[1] Ù v[p] ³ v[2] Ù  v[p] ³ v[3] }

como precondición no es necesario pedir nada especial antes, es decir se puede utilizar un predicado que no exige nada a las variables involucradas en ese punto, ese predicado es el predicado Cierto.

La postcondición es la que se pretendía obtener:

 {1<=p<=3 Ù v[p] ³ v[1] Ù v[p] ³ v[2] Ù  v[p] ³ v[3] }

es decir, en p se devuelve el índice del mayor valor del vector.

Observando el programa anterior se puede comprobar que no sería difícil generalizarlo para vectores de dimensión N genérica, utilizando un bucle para la implementación:

p:= 1;

para i:= 1 hasta N hacer (P) 

    si v[i]>v[p] entonces p:=i;

fpara

el predicado (P) que ha de cumplirse en la entrada a las instrucciones al cuerpo interior del bucle será (generalizando los predicados intermedios en el programa ...)

(1<=p <=N  Ù para todo a tal que 1<= a<= i se tiene que v[p]>=v[a] )

este es el denominado Invariante del bucle (ver Peña Cap 4), un predicado que se cumple siempre en cada entrada a las intrucciones al cuerpo interior del bucle y que, por tanto, se cumplirá también cuando el bucle finalice, momento en que i valdrá N y se tendrá :

(1<=p<= N Ù para todo a tal que 1<=a<= N se tiene que v[p]>=v[a] )

que equivale a decir que p es el índice del mayor de los elementos del vector v. 

Obsérvese la técnica seguida en el diseño: se van ejecutando instrucciones que aseguren algunas de las condiciones que se piden en los predicados, de forma que el predicado previo a dichas instrucciones pueda ser menos exigente. Así hasta obtener un predicado fácil de cumplir en el punto inicial del segmento de programa o algoritmo.

El establecimiento de predicados de la forma más compacta y menos ambigua posible requiere de un lenguaje concreto que se expondrá en posteriores apartados y que puede verse en Peña Cap. 2. 

Conclusiones

El lenguaje de predicados y las técnicas asociadas son una herramienta importante en:

• La especificación de módulos de software independientes, permitiendo una clara separación entre funcionalidad e implementación.

• El diseño sistemático de algoritmos. Éste, como indica J.L. Balcázar, es uno de los puntos clave de la programación metódica. Las técnicas de predicados no sirven tanto para verificar algoritmos ajenos, como para guiar el diseño y permitir una metodología sistemática y rigurosa, como se verá más adelante en los apartados de diseño recursivo e iterativo.

• La verificación de segmentos de programa. 

Todo ello requiere un cierto dominio de las técnicas básicas, los operadores lógicos y cuantificadores y la relación mental que siempre ha de mantenerse entre establecimiento de predicados sobre las variables significativas de un programa y estado del mismo. 

Para practicar la verificación y derivación de instrucciones puede ser útil la siguiente colección de ejercicios:

derivacion_instrucciones.pdf