PDF de programación - Capítulo 2 - Problemas, programas, estructuras y algoritmos

2.4. Especificaciones formales constructivas

61

incluyendo el anterior comportamiento como aserto invariante del tipo Pila, el resultado
final de la expresión sería: “La pila está vacía”.

2.4. Especificaciones formales constructivas

En una especificación formal constructiva, u operacional, el significado de las ope-
raciones se establece mediante las cláusulas de precondición y postcondición. Al con-
trario de las especificaciones algebraicas –donde las operaciones se definen a través de
las relaciones entre ellas– en las especificaciones constructivas cada operación es descrita
independientemente de las demás. Por este motivo, se dice que en el método algebraico el
significado de las operaciones es implícito, mientras que en el constructivo el significado
es explícito.

El formato de notación utilizado en las especificaciones constructivas coincide con
el ya visto para las algebraicas en las partes Nombre, Conjuntos y Sintaxis. La diferencia
está en la parte Semántica, que contendrá la pre- y postcondición de cada operación.

2.4.1. Precondiciones y postcondiciones

La precondición y la postcondición son condiciones lógicas que indican, respectiva-

mente, los requisitos de una operación y su efecto.

Precondición. Relación lógica que deben de cumplir los valores de entrada para
que la operación se pueda aplicar con garantías de producir una ejecución correcta.

Postcondición. Relación lógica que se cumple con los valores de salida después de
ejecutar la operación, siempre que se cumpliera la precondición.

Las pre- y postcondiciones son también llamadas asertos: afirmaciones que deben
ser ciertas antes y después de ejecutar una operación, respectivamente. Para cada opera-
ción <nombre> definida en la parte Sintaxis, dentro de la parte Semántica deben aparecer
las dos siguientes cláusulas:

pre-<nombre>(<param entrada>)::= <condición lógica>
post-<nombre>(<param entrada>;<param salida>)::= <condición lógica>

Ejemplo 2.14 Especificación constructiva de una operación maximo, que tiene como en-
trada dos números reales y devuelve como resultado el mayor de los dos.
maximo: R × R → R

pre-maximo(x, y)::= verdadero
post-maximo(x, y; r)::= (r ≥ x) ∧ (r ≥ y) ∧ (r = x ∨ r = y)

Ejemplo 2.15 Especificación constructiva de una operación max restring, máximo res-
tringido, que calcula el máximo de dos números, pero sólo se puede aplicar a enteros
positivos.
max restring: Z × Z → Z

pre-max restring(x, y)::= (x > 0) ∧ (y > 0)
post-max restring(x, y; r)::= (r ≥ x) ∧ (r ≥ y) ∧ (r = x ∨ r = y)

62

Capítulo 2. Abstracciones y especificaciones

Como se ve en los ejemplos anteriores, la postcondición no debe indicar necesaria-
mente un valor concreto para el resultado. Simplemente expresa una condición lógica que
es cierta. Igual que en las especificaciones algebraicas, es posible usar condicionales de
la forma SI <condición> ⇒ <valor si cierto> | <valor si falso>. Además, también se
pueden usar los cuantificadores ∀ y ∃.

Ejemplo 2.16 Especificación constructiva de una operación BusquedaBinaria, que realiza
una búsqueda binaria dentro de un array de elementos de un tipo parametrizado T.
BusquedaBinaria: Array[T] × T → N

pre-BusquedaBinaria(a, t)::= ∀i = 11, ...,Tamaño(a) − 1; a[i] ≤ a[i + 1]
post-BusquedaBinaria(a, t; n)::= SI t < a[1] ⇒ n = 0 | SI t > a[Tamaño(a)] ⇒
n =Tamaño(a) + 1 | (a[n] = t) ∨ (a[n] < t < a[n + 1])
Se supone que la operación Tamaño, definida sobre arrays, devuelve el número de
elementos del array, y que el tipo parametrizado T tiene definidas operaciones de com-
paración entre valores del tipo.

En este caso, la precondición expresa el requisito de que el array de entrada debe
estar ordenado de menor a mayor. En tal caso, la operación devuelve la posición donde se
encuentra, o se debería encontrar, el valor buscado. Este resultado es lo que se indica en
la postcondición. Pero se puede ver que la postcondición no dice nada de cómo se busca
el elemento. Es un detalle de implementación que no debe aparecer en la especificación.

Error frecuente 2.1 Es muy importante no confundir especificación e implementación:
la especificación describe el resultado esperado de una operación; la implementación es
un trozo de código que calcula ese resultado. Por lo tanto, la especificación debe ser
independiente de la implementación. Sin embargo, el método constructivo permite definir
especificaciones que son muy próximas a implementaciones. Por ejemplo, una posible
postcondición para la operación máximo podría ser:

post-maximo(x, y; r)::= SI x > y ⇒ r = x | r = y
En este ejemplo sencillo, se ve más claramente el significado de la operación. Sin
embargo, en general, hay que evitar este tipo de especificaciones porque mezclan especi-
ficación con implementación, ofreciendo al usuario de la abstracción detalles innecesarios
de programación.

2.4.2. Especificación como contrato de una operación

El significado de una especificación constructiva es: si se cumple la precondición y
se ejecuta la operación, entonces se puede asegurar que se cumple la postcondición. Una
buena analogía para una especificación de este tipo es un contrato –que conlleva ciertos
derechos y obligaciones– que se establece entre el que implementa la operación y el que
la usa. La idea de la especificación como un contrato es mostrada en la figura 2.3.

2.4. Especificaciones formales constructivas

63

Figura 2.3: La especificación de un producto software como contrato entre el que lo pro-
grama y el que lo usa.

En concreto, el contrato en la especificación constructiva estipula lo siguiente:

IMPLEMENTADOR

Derechos
Supone que se cumple la precondición,
sin preocuparse de qué hacer en caso
contrario. Esto le evita tener que com-
probarla.

Obligaciones
Debe hacer los cálculos necesarios para
conseguir que se cumpla la postcondi-
ción al acabar la ejecución de la opera-
ción.

USUARIO

Obligaciones
Es el responsable exclusivo de garantizar
que se cumpla la precondición, antes de
ejecutar la operación.

Derechos
Obtiene los resultados que se indican
en la postcondición, siempre que haya
cumplido sus obligaciones.

Así que el responsable de comprobar la precondición es el usuario de la operación,
y el responsable de garantizar la postcondición es el implementador de la operación. Este
reparto de responsabilidades ayuda a simplificar la construcción de programas, puesto que
se evitan comprobaciones redundantes e innecesarias.

Pero, ¿qué ocurre si no se cumple una precondición? Simplemente no se garantiza
que se cumpla la postcondición. En tales casos, el creador de la especificación puede elegir
básicamente entre dos opciones:

- No especificar nada. En caso de error en los parámetros de entrada, el efecto será im-
previsible; puede que en algunas situaciones se cumpla la postcondición, en otras
no, o incluso puede que el programa se cuelgue.

- Especificar un comportamiento estándar en caso de fallo de la precondición. Este
comportamiento puede ser, por ejemplo, interrumpir la ejecución del programa,
seguir como si no se hubiera ejecutado la operación, indicar la situación en una
variable de error o provocar una excepción.

64

Capítulo 2. Abstracciones y especificaciones

En la práctica, el uso de excepciones suele ser la solución más utilizada. La eje-
cución de una excepción implica que la operación interrumpe su ejecución. El control
pasa al procedimiento que ha ejecutado la llamada, que tendrá definido un código para el
tratamiento de excepciones. En caso contrario, la excepción pasará al que lo ha llamado
y así sucesivamente.

Una tercera opción sería incluir el tratamiento del error dentro de la operación
que la implementa y también dentro de la propia especificación formal. Igual que en la
especificación algebraica, se debería indicar en la sintaxis que la operación puede devolver
un mensaje de error. Por ejemplo, vamos a suponer que en la especificación constructiva
de la operación máximo restringido incluimos el tratamiento de errores, en caso de que
alguno de los parámetros no sea positivo. La especificación sería:
max restring2: Z × Z → Z ∪ {“Error de precondición”}

pre-max restring2(x, y)::= verdadero
post-max restring2(x, y; r)::= SI (x > 0) ∧ (y > 0)
⇒ (r ≥ y) ∧ (r ≥ y) ∧ (r = x ∨ r = y)
| “Error de precondición”

Está claro que esta elección rompe la filosofía de los contratos: el implementador
comprueba y trata las condiciones de error en los parámetros de entrada, lo cual no debería
ser su responsabilidad. Al definirlo de esta manera, se puede decir que la especificación
“oculta” los verdaderos requisitos de la operación, puesto que la precondición siempre es
cierta. En cierto sentido, el cliente es “engañado”: cree que puede ejecutar la operación
sin problemas, pero se encuentra con mensajes de error inesperados.

2.4.3. Necesidad de un modelo subyacente

Si el TAD que se está definiendo es un tipo complejo, expresar las precondiciones y
las postcondiciones usando únicamente operaciones lógicas puede ser difícil o inviable. En
esos casos es posible utilizar otro tipo de datos como tipo subyacente, en el cual se basa
la especificación del tipo que está siendo definido. Este tipo o modelo subyacente debería
estar especificado formalmente, ya sea por el método algebraico o por el constructivo.

Un ejemplo de TAD donde resulta necesario un modelo subyacente son los tipos
colección o contenedores. Para definir de forma constructiva cualquier contenedor es nece-
sario usar como modelo subyacente algún otro tipo contenedor. En última instancia nece-
sitaremos algún TAD contenedor cuya definición no esté basada en otro contenedor; este
tipo subyacente será especificado de forma algebraica.

Vamos a ver como ejemplo la especificación formal constructiva de los TAD genéricos
Pila[T] y Cola[T]. La definición de estos tipos se basará en el modelo subyacente Lista[T],
el cual será definido de forma alg