Programación metódica

Especificación. Instrucciones
básicas

Para comprobar si un programa ha sido escrito
adecuadamente se suelen efectuar algunas ejecuciones de prueba
que permitan conocer su comportamiento. Intentamos saber si
calcula los resultados deseados, y es, por tanto,
correcto.

Mediante estas ejecuciones, en efecto, se puede detectar
la presencia de algún error, y en muchos casos resulta
sorprendentemente laboriosa su identificación y
reparación, sobre todo en caso de programas extensos y
complejos. Pero puede darse un caso aún peor: que las
pruebas no revelen errores, y éstos aparezcan más
tarde, cuando el daño es mayor.

Un segundo inconveniente que ofrece esta
validación dinámica es que, una vez detectada la
existencia de errores, la información que obtenemos sobre
los puntos del programa en que se encuentran es muy
escasa.

La alternativa será una validación
estática, que consista en obtener información a
priori sobre el comportamiento del programa mediante el
análisis de su propio texto. Este análisis debe ser
capaz de demostrar que los resultados que el programa proporciona
son los deseados, o bien de detectar la presencia de errores e
identificarlos completamente; este proceso se llama
verificación.

La construcción de programas ya verificados se
denomina "derivación", y resulta mucho más
importante en la práctica que la
verificación.

La corrección se define entonces como la
coincidencia entre el comportamiento deseado del programa y su
comportamiento real.

Para expresar el comportamiento esperado de un algoritmo
usaremos especificaciones. Estas constarán de una
precondición (condiciones que deben cumplir los datos del
programa) y una postcondición (relaciones que deben
existir entre los datos recibidos y los resultados
obtenidos).

Un algoritmo es considerado como una sucesión de
estados con instrucciones entre cada estado.

ESTADOS, ASERTOS Y EXPRESIONES

El análisis de un programa puede hacerse en
términos de un conjunto de estados iniciales admisibles y
un conjunto de estados finales apropiados. Para describir
conjunto de estados utilizaremos asertos.

Dado un conjunto de variables (que pueden o no tener un
valor), un estado es una aplicación de este
conjunto de variables en el conjunto de sus valores, de manera
que se asocie a cada variable un valor coherente con su tipo. Si
se observa el valor de las variables de un programa en un cierto
momento obtenemos el estado del programa en ese
momento.

Un aserto, predicado o
aserción es una expresión lógica que
involucra las variables del programa que usamos para expresar el
comportamiento de dicho programa en ciertos momentos. Los asertos
no son las únicas expresiones lógicas que usamos.
Hay asertos no evaluables (no pueden aparecer en las
instrucciones del programa), estas expresiones son las
expresiones cuantificadas (expresiones introducidas por un
cuantificador) y las operaciones ocultas (expresiones expresadas
con un nombre).

CUANTIFICDORES Y VARIABLES

Un cuantificador es una abreviatura de una
secuencia de operaciones que requiere ir asociado a una
variable ligada o ciega, que es simplemente un
identificador, y a un dominio, que indica el conjunto de
valores que permitimos tomar a la variable ligada y que
frecuentemente es un intervalo de los naturales. La
expresión así obtenida denota la repetición
de la operación sobre todos los valores del dominio.
Usaremos con frecuencia los siguientes
cuantificadores:

Es concebible aplicar algunos cuantificadores sobre un
dominio vacío. El resultado del contador sobre un dominio
vacío es cero. La iniciación de un bucle de la
iteración y el caso directo de la recursividad se realizan
mediante el neutro o el dominio vacío de los
cuantificadores.

Cuadro resumen de los
cuantificadores

Cuando el dominio no es nulo, podemos separar uno de sus
elementos y reducir en uno el dominio del cuantificador. El
elemento separado se combina con el cuantificador reducido,
mediante la correspondiente operación binaria.

De la misma manera, podemos separar un elemento
arbitrario del dominio de un cuantificador cualquiera, salvo que
sea vacío, combinándolo con el resto mediante la
operación binaria asociada al cuantificador.

El cuantificador contador para poder separarlo en dos se
necesita una alternativa, una condición.

Las variables que aparezcan en los asertos podrán
ser de los siguientes tipos:

–Variables ligadas o ciegas: está
vinculada a un cuantificador, y puede ser sustituida por
cualquier otra sin que se modifique el significado de la
expresión.

–Variables libres: dentro de este grupo se
encuentran:

·Del programa: que denotan, en cada punto del
mismo, el último valor que se les haya
asignado.

·Iniciales: se usan para denotar un valor que
sólo se conoce en un punto diferente de la
ejecución del programa.

Conviene evitar el uso del mismo nombre para variables
del programa y variables ligadas.

Cada aserto puede ser considerado como una
descripción de un conjunto de estados: aquellos en los que
los valores de las variables hacen que el aserto evalúe a
cierto.

SUSTITUCIONES

Una importante operación que se puede realizar
sobre los asertos es la de sustitución, que
permitirá razonar sobre instrucciones de
asignación.

En ningún momento se debe utilizar una variable
ligada o ciega y una libre con el mismo nombre, ni siquiera en
distintos asertos o expresiones. De no ser así basta dar
nuevos nombres a las variables ligadas manteniendo el
significado.

Sea A un aserto, x una variable y E una expresión
del mismo tipo que x. Denotaremos:

AxE

el aserto que se obtiene sustituyendo todas las
menciones de la variable x en A por la expresión
E.

Al hacer un cambio se ha de ir con cuidado de no poner
los mismos símbolos a las variables ligadas y a las
variables libres ya que podrían cambiar el significado el
aserto.

ESPECIFICACIÓN PRE/POST

Al expresar, mediante un aserto, las condiciones que se
imponen a los datos, se está restringiendo el conjunto de
estados en que se puede poner en marcha el programa con
garantías de funcionamiento correcto. Este aserto que
impone condiciones a los datos s denomina
precondición. Cuanto más débil sea
esta precondición, más útil será el
programa, ya que podrá emplearse en más casos. De
manera dual, el aserto que expresa las propiedades de los
resultados del algoritmo se denomina
postcondición.

Una especificación pre/post para un programa P se
escribe: {A} P {B}

y denota que se requiere del programa P que, si comienza
a funcionar en un estado que satisfaga A, termine en un tiempo
finito y en un estado que satisfaga B. La especificación
describe el comportamiento esperado del programa P.

Verificar el programa consiste entonces en "demostrar"
que cumple su especificación.

Supongamos que se ha demostrado {A} P {B}.
Entonces:

-Si A(A" entonces {A"} P {B} es cierto y además
se refuerza el aserto.

-Si B(B" entonces {A} P {B"} es cierto y además
se debilita el aserto.

Frecuentemente el fragmento de programa a diseñar
no va a considerarse aislado, sino que es parte del desarrollo de
un programa más complejo. En este caso, puede ser
conveniente dar un nombre a este fragmento de programa, y
seleccionar unos parámetros de entrada y unos resultados.
Lo haremos mediante la función.

Para especificar la función necesitamos saber
qué variables representan datos y cuales resultados. La
especificación constará de tres partes: cabecera,
pre y postcondición. La cabecera indica el nombre de la
función y como se llaman y de que tipo son los
parámetros y las variables locales en las que se
calcularán los resultados. La precondición
involucrará los parámetros y la
postcondición los resultados.

La sintaxis para presentar la cabecera de una
función es:

funció nom (parámetros)
ret resultados

{Pre}

variables locales

{Post}

ret resultados

ffunció

Parámetros o resultados d distintos se separan
por ";".

Una vez calculados los resultados, todos ellos
aparecerán al final del cuerpo de la función en una
instrucción "dev" o "ret", que representa la
devolución de resultados al punto en que se produjo la
llamada. Sólo puede haber una instrucción dev o ret
en cada función, y ha de estar situada como última
instrucción a realizar.

TEMA 2:

Verificación y
derivación

SEMÁNTICA AXIOMÁTICA

En esta sección se presenta la definición
del lenguaje de programación:

–Instrucción nula: corresponde a
continuar la ejecución "sin hacer nada", es decir, sin
modificar el estado de las variables. Su denotación
es:

Es decir todo lo que se cumple antes se sigue cumpliendo
después.

–Asignación simple: modificación
de una determinada variable, y por lo tanto conlleva una
modificación del estado. La asignación simple
sólo afecta a una variable.

–Asignación múltiple: Dada una
cierta cantidad de variables distintas y expresiones y suponiendo
que los tipos coinciden denotamos:

la instrucción de asignación
múltiple, simultánea, del valor de cada
expresión a su variable correspondiente. La
característica de simultaneidad es importante, dado que es
factible que algunas de las variables x aparezcan en algunas de
las expresiones E y deben ser interpretadas con el valor que
tengan previamente a la asignación.

–Composición: es la composición
secuencial de otras acciones para ser ejecutadas en el orden
indicado. Se denota separando las acciones que la forman con un
punto y coma: P1;P2. Su definición semántica es
como sigue: para demostrar {A1} P1;P2 {A3} es preciso encontrar
un A2 tal que se pueda demostrar {A1} P1 {A2} y {A2} P2
{A3}.

–Alternativa: esta instrucción permite
seleccionar acciones a ejecutar en función del estado en
que se encuentre el algoritmo. Se basa en el concepto de
instrucción protegida, que es un par formado por
una expresión booleana llamada protección y una
instrucción cualquiera; si la protección
evalúa a cierto diremos que está abierta y
cerrada en caso contrario. La idea es que sólo
estará permitido ejecutar una instrucción protegida
si su protección está abierta. La sintaxis
será:

donde cada rama corresponde a una instrucción
protegida; por tanto las expresiones Bi habrán de ser tipo
booleano. Se ejecuta evaluando todas las protecciones; si todas
ellas están cerradas, la ejecución del algoritmo
aborta; y en caso contrario se selecciona
indeterminístacmente una protección abierta y se
ejecuta su instrucción asociada.

Para comprobar si la precondición A1 es
válida respecto de la postcondición A2, han de
verificarse los siguientes puntos:

-Que al menos una de las protecciones esté
abierta: A1 ( B1(B2(…(Bn

-Que cualquier protección abierta dé
lugar, tras la ejecución de la instrucción
protegida, a un estado que cumpla A2: {A1 ( Bi} Si
{A2}.

–Llamada a una función: cuando se
produzca una llamada a una función especificada mediante
pre y postcondición, y con el fin de facilitar el
razonamiento, la escribiremos en una instrucción de
asignación:

debemos demostrar, justo antes de esta
instrucción, que las expresiones que se pasen como
argumentos cumplen la pre de la función; a
continuación de esta asignación, las variables
sobre las que se han asignado los resultados cumplirán la
postcondición. Este cambio de nombre sigue los mismos
criterios que las sustituciones de variables por
expresiones.

Para:

DERIVACIÓN

Podemos deducir instrucciones algorítmicas a
partir de su especificación, proceso que se denomina
derivación. La construcción del algoritmo no es
completamente mecánica y sigue requiriendo ciertas dosis
de inventiva, pero el proceso proporciona abundantes sugerencias
y datos sobre la corrección de las decisiones
tomadas.

Este proceso es especialmente útil para concretar
los detalles que pueden dificultar, por el grado de
precisión que requieren, la tarea de programar:
inicializaciones, conjunciones y disyunciones en las condiciones
de los bucles, decisión entre comparaciones "menor que" o
menor o igual" y similares.

En un proceso de derivación, la
postcondición resulta más relevante y proporciona
mucha más información que la precondición,
sin que ésta sea irrelevante. El análisis de la
postcondición es por tanto un buen método para
desarrollar algoritmos. Mencionemos algunas
consideraciones:

-Si en la postcondición aparecen igualdades entre
variables del programa y expresiones, puede satisfacerse mediante
asignaciones simples o múltiples.

-Si aparecen disyunciones se puede intentar
diseñar una alternativa.

-Si aparecen conjunciones se puede intentar
diseñar una alternativa o considerar cada una de ellas
aisladamente, e intentar satisfacerlas por separado mediante
asignaciones.

Ejemplos de derivación en el libro a partir de la
pag 34.

TIPOS ESTRUCTURADOS DE DATOS

Es preciso que para cada tipo de datos que nos sea
conveniente emplear, encontrar las maneras apropiadas de
:

1/ ampliar el repertorio de operaciones disponibles para
formar expresiones.

2/ ampliar el repertorio de procesos deductivos de
manera que podamos manipular algebraicamente estas
expresiones.

3/ y poder efectuar razonamientos cuya validez no
dependa de posibles cambios en la representación del
tipo.

Ante la idea de usar un tipo nuevo, se decidirá
un nombre para éste y tal vez para otros tipos auxiliares,
y nombres para las operaciones que se vayan considerando
necesarias; de esta forma habremos logrado la ampliación
del repertorio de operaciones. A estos nombres se
añadirán descripciones de las propiedades que han
de cumplir estas operaciones, con lo cual obtendremos la
ampliación de los procesos deductivos.

En concreto, la información de la que necesitamos
disponer para utilizar un tipo de datos, y para razonar sobre sus
operaciones asociadas, vendrá dada por una
especificación algebraica, también llamada
ecuacional, del tipo. Ésta consta de dos partes: la
signatura y las ecuaciones.

SIGNATURA

La signatura es una simple declaración de
identificadores: ha de aparecer un identificador, llamado
género, por cada tipo que intervenga en el proceso,
y ha de aparecer un nombre de operación por cada
operación que se precise. Cada uno de éstos ha de
llevar asociada su aridad, también denominada
perfil, y que consiste en una descripción precisa
del número de argumentos de la operación, del
género de cada uno de ellos, y del género del
resultado. Esta información es exactamente la que nos
permite construir expresiones con estas operaciones. Las
expresiones que se pueden formar con las operaciones de una
signatura se denominan también en ocasiones
términos sobre esa signatura.

Desde el punto de vista de programación, el
intento de aplicar una operación en un caso en que
ésta está indefinida se considera un error de
ejecución.

ECUACIONES

Las ecuaciones de la especificación describen la
manera de operar algebraicamente con las expresiones que
contienen operaciones de la signatura.

En su forma más simple, una ecuación de
una especificación algebraica consiste en un par de
términos con variables; se denota relacionándolos
mediante el signo "(". Significa que, cualesquiera que sean los
valores de las variables, ambos términos han de denotar
siempre el mismo valor; más concretamente, puesto que
pueden aparecer operaciones parciales, la ecuación
significa que, o bien ambas expresiones son error, o bien ambas
expresiones pueden ser evaluadas correctamente, y en este caso
los valores obtenidos siempre coinciden.

Ejemplo (booleanos)

LISTAS

Disponen simplemente de dos operaciones constructoras:
la que crea una lista nula y la que coloca un elemento adicional
en una lista. Añadimos otra operación: la
concatenación denotada _++_.

Suele a veces emplearse una notación algo
informal, pero más cómoda, usando los corchetes.
Por ejemplo, si e1, e2 i e3 son elementos, la lista e1:(( se
denota (e1(, y la lista e1:(e2:(e3:( ()) se denota (e1, e2, e3(.
La operación ":" se denomina a veces cons porque permite
construir listas, y la operación "++" se denomina
concatenación, denotada a veces concat o incluso cat en
lugar de "++".

Añadimos también una operación long
que nos proporciona la longitud de la lista.

PILAS

Género: pila

Parámetros: elementos

Operaciones: p_vacia: —————>
pila

apilar: elem x pila —-> pila

cima: pila ————->elem ; da el último
elemento de la pila no lo saca

desapilar: pila ——–> pila;saca el último
elemento

vacía: pila ————>bool; nos dice si la
pila está vacía.

Ecuaciones: (x: elem, (p: pila.

· cima (p_vacia) ( error

· cima (emp (x, p)) ( x

· desemp (p_vacia) ( error

· desemp (emp (x, p)) ( p

· vacía (p_vacia) ( cierto

· vacía (emp (x, p)) ( falso

Usaremos a veces como función oculta la
función longitud o altura y la función suma de una
pila, que corresponde exactamente a la que hemos denominado long
en el caso de las listas:

Operaciones: long: pila ———>
natural

suma: pila ———> entero

Ecuaciones: (x: elem, (p: pila.

· long (p_vacia) ( 0

· long (emp (x, p)) ( 1+altura (p)

· suma (p_vacia) ( 0

· suma (emp (x, p)) ( x + suma (p)

La operación p_vacia corresponde a "[]"y apilar
corresponde a ":". Estas dos operaciones son las constructoras
del tipo.

Las ecuaciones indican que cima y desapilar,
conjuntamente, forman la operación inversa a apilar;
más aún, es posible demostrar el hecho,
intuitivamente claro, de que si p es una pila no nula

emp (cima (p), desemp (p)) ( p

Demo: si p no vacía => p=emp (x,
p")

emp (cima (emp (x, p")), desemp (emp(x, p"))( ( emp (x,
desemp (emp (x, p"))( ( emp (x, p") ( p

También se puede demostrar:

long (desemp (p)) ( long (p)-1

suma (desemp (p)) ( suma
(p)-cima(p)

Demo: suma (p) = suma (desemp (p)) + cima (P)

si p no es vacía => (x, p": p=emp (x,
p")

suma (desemp (p))+cima (p) ( suma (desemp (emp (x,
p"))(+ cima (emp (x, p")( ( suma (p") + x. Suma (p) ( suma(emp
(x, p")( ( x+suma (p").

Denominamos pila a esta estructura porque, si
consideramos una variable de este tipo y efectuamos sobre ella
varias operaciones de apilar, el elemento más reciente es
el único accesible a través de la operación
cima, y el que se apiló el primero es el que más
operaciones de desapilar requiere para su reaparición
(estructura LIFO: last in first out).

COLAS

Cuando un elemento pide turno en una cola en la que ya
había otros elementos, el primero sigue siendo el mismo, y
que, de no haber otros, el primero es el recién llegado.
Al avanzar la cola desaparece el primero: si éste era el
recién llegado, por tanto el único, la cola queda
vacía; de lo contrario, no hay diferencia entre
incorporarlo a la cola antes o después del
avance.

En las colas disponemos de una operación
long que nos proporciona la longitud de una cola y
también de la función suma.

ARBOLES

En muchas ocasiones consideraremos enriquecido el tipo
árbol binario con tres operaciones adicionales: la que
calcula la altura o profundidad del
árbol, la operación tam que nos da el
tamaño y la operación suma. La altura es
el máximo número de elementos que es posible
encontrar al seguir una rama del árbol.

TABLAS

La tabla más simple es aquella que se encuentra
completamente indefinida, es decir, no asocia valor a
ningún índice. La obtendremos mediante la
operación crear. Se construyen nuevas tablas, a
partir de crear, asignando valores a los índices.
Para ello contamos con la operación assig. Dado
que cada índice puede tener asociado únicamente un
valor, si se asigna uno nuevo a un índice que ya lo tiene,
el valor anterior deja de estarle asignado. También
podemos consultar el valor asociado a un índice en un
tabla, es decir, evaluar la función parcial en un punto,
mediante la operación val; dado que esta
operación provoca un error si el índice consultado
no tiene un valor asignado, es conveniente disponer de un medio
para averiguar si se ha definido o no un valor asociado a un
índice dado: def.

La penúltima ecuación indica que en caso
de asignar valor repetidas veces a un mismo índice, tan
solo el último es válido. La última, que el
orden de asignación de valores a índices distintos
es indiferente.

Los vectores son un caso particular de las tablas,
especialmente importante por la eficiencia de su
implementación en la mayoría de las arquitecturas
de computadores. Se trata de tablas en las que los índices
corresponden a lo que se denomina un "tipo enumerado". Nos
limitaremos aquí al caso más frecuente, en el que
cada índice en un número natural. La
característica principal de los vectores es la existencia
de un índice mínimo y un índice
máximo, sin que sea posible definir ni consultar el valor
para naturales que no se encuentren entre esos índices;
más aún, esta restricción se impone
provocando un error de ejecución si se intenta operar
fuera de los índices permitidos.

El principio de
inducción

La técnica de inducción completa, para
demostrar propiedades sobre los números naturales
es:

Para demostrar que una propiedad de un tipo de datos, es
preciso identificar en la especificación el conjunto de
operaciones constructoras. Una vez identificado este conjunto, se
considera cada una de las constructoras, y se justifica que un
término cuya operación más externa es esta
constructora cumple siempre la propiedad que deseamos,
suponiendo, si es preciso, que todos los argumentos a los que se
aplica la cumplen igualmente. De esta forma, los términos
más simples van "propagando" la propiedad hacia los
más complicados.

Hay que considerar, para cada valor del tipo, el
número mínimo de veces que se aplican los
constructores para obtener un valor del tipo. Por ejemplo, en el
tipo pila, podemos considerar que los teoremas
inductivos razonan por inducción sobre la altura
de la pila, que es siempre un número natural y que
coincide con el número de veces que hemos aplicado la
operación apilar; de manera similar, los teoremas
inductivos sobre el tipo cola actúan por
inducción sobre la longitud, el número de
elementos de la cola, que es el número de veces que se ha
aplicado pide-turno (demanar-torn), y en los
árboles sobre el tamaño del árbol,
o sea, número de elementos que aparecen en las
raíces de los diversos subárboles, que es asimismo
el número de veces que se aplica
plantar.

Para poder plantear la inducción sobre
estructuras diferentes de los números naturales es preciso
dotar de significado al símbolo "<". La noción
apropiada es la de preorden. Un preorden sobre un conjunto
A es una relación binaria reflexiva y
transitiva.

Programas
recursivos

Para aprovechar la potencia del computador es
indispensable poder describir una ejecución larga mediante
un texto breve, y la manera natural de hacerlo es mediante la
repetición de cálculos. Entre las posibilidades que
ofrecen los lenguajes de programación suelen presentarse
dos medios para repetir cálculos: las instrucciones
iterativas, que expresan sintácticamente un bucle o
repetición, y la recursividad, es decir, la posibilidad de
que un subprograma se active a sí mismo, o en nuestro caso
que una función contenga, entre sus instrucciones, una
llamada a sí misma.

En todo programa recursivo, ha de haber al menos una
instrucción alternativa. En efecto, el texto debe incluir
activaciones del propio programa, por ser éste recursivo,
pero no se ejecutan en todos los casos, pues de lo contrario la
recursividad no terminaría; por tanto, han de estar en una
instrucción alternativa en la cual no todas las ramas
provoquen recursividad. Distinguiremos pues en esa alternativa
dos tipos de ramas: los casos directos, que no provocan
llamadas recursivas, y los casos recursivos.

Así pues, los programas recursivos más
sencillos obedecen al siguiente patrón:

Teniendo en cuanta las reglas de la instrucción
alternativa, hemos de comprobar que todos los casos posibles
están cubiertos, lo cual es inmediato en este programa, y
hemos de verificar individualmente cada rama.

No nos planteamos verificar completamente f,
sino solamente f aplicada a x; asociamos a cada x que
pueda aparecer como parámetro de la función un
número natural t(x); y suponemos, como hipótesis de
inducción, que f funciona correctamente para
todos aquellos parámetros cuyo natural asociado es
inferior.

La función t(x) recibe el nombre de
función de cota, o también función
limitadora. Esta función de cota, a la vez que valida el
razonamiento por inducción, garantiza la
terminación de la secuencia de llamadas recursivas, ya que
cada una ha de tener un valor natural t(x) estrictamente inferior
al de la anterior, y en los naturales esto no puede ocurrir
indefinidamente.

En resumen, los pasos que hay que dar para verificar un
programa recursivo que corresponda al esquema dado, con un
único caso directo y un único caso recursivo,
serían:

FUNCIONES DE COTA

Suponemos que un programa recibe, como
parámetros, dos números naturales (m, n), y que
consideramos qué les puede ocurrir en el momento de
efectuarse las llamadas recursivas. Si siempre decrece el mismo,
éste define la cota. Si siempre decrece uno de ellos pero
no siempre el mismo, y entonces el otro se mantiene, podemos
recurrir a la expresión m+n. Pero cuando el que no
decrece, en lugar de mantenerse, crece, si bien nunca alcanzando
al otro, podemos seleccionar como natural sobre el que realizar
la inducción el mayor de entre ellos, max(m,
n).

En otras ocasiones aparece un parámetro booleano
(b) y en alguna de las llamadas es el único que cambia;
supongamos que pasa de cierto a falso. En este caso, incluimos en
la función de cota un término n(b) definido por
n(cierto)=1 y n(falso)=0, lo que asegura el decrecimiento. En
caso de pasar de falso a cierto, el término que
añadimos es 1-n(b).

Supongamos ahora que los parámetros son de tipos
más complejos. Si se trata de una pila, la cota puede ser,
al igual que en los teoremas inductivos, la función
altura, que asocia a cada pila el número de elementos de
que consta, aplicada a alguna de las pilas que se reciben como
parámetro. Igualmente en el caso de las colas, la longitud
puede jugar idéntico papel. En cuanto a los
árboles, disponemos de dos funciones que nos permiten
obtener un número natural: el tamaño y la altura;
con frecuencia es posible elegir, indistintamente, cualquiera de
los dos.

METODOLOGÍA

Diremos que un programa presenta recursividad
lineal si cada llamada recursiva genera, como mucho, otra
llamada recursiva; en caso contrario, si alguna llamada puede
generar más de una llamada adicional tendremos
recursividad múltiple.

Para diseñar un programa recursivo ante todo se
ha de preparar la especificación de la función,
escribiendo su cabecera e identificando precondición y
postcondición. La precondición será un
aserto que involucre los parámetros formales en que se
reciben los datos, y se puede suponer que se cumple antes de
ejecutarse la primera instrucción del cuerpo de la
función; la postcondición involucrará
además a los nombres que se hayan elegido para los
resultados, y se deberá demostrar que es cierta antes de
efectuar la instrucción de devolución.

Luego es preciso concretar la función cota, es
decir, la expresión sobre la que se realizará la
inducción: ha de asociar a cada valor posible de los
parámetros un número natural.

Después se procede a analizar los posibles casos
que se puedan presentar, intentando identificar, al menos, un
caso directo y un caso recursivo; es preciso asegurarse, como en
toda instrucción alternativa, de que se cubren todos os
casos que puedan aparecer.

A continuación será preciso diseñar
el fragmento de programa que resuelve cada caso, conjuntamente
con su verificación; por supuesto, en esta fase pueden
aparecer nuevas instrucciones de alternativa. Al programar los
casos recursivos será preciso suponer, como
hipótesis de inducción, que las llamadas recursivas
funcionan correctamente, es decir, que satisfacen la
especificación.

En resumen, los pasos a dar son:

– especificación de la función;

– análisis de casos;

– identificación de la función de cota,
que ha de estar bien definida;

– programación y verificación de cada
caso;

– validación de la inducción: la
función de cota decrece estrictamente en las
llamadas.

Inmersión
de algorismos

AL desarrollar un diseño recursivo de un
programa, puede detectarse la necesidad de generalizar la
función que se está diseñando, bien sea para
facilitar los razonamientos y completar el programa, bien porque
no se encuentra una solución recursiva, o bien porque se
desee obtener soluciones alternativas, quizá más
eficientes. En estos casos podemos recurrir al concepto de
inmersión.

Una inmersión de una función dada es
simplemente una generalización de ésta, que tiene
argumentos adicionales y/o resultados adicionales ;esta
función más general ha de buscarse de modo que,
fijando determinados valores para los argumentos adicionales y
descartando los resultados adicionales, se recupere la
función inicial.

REFORZAR LA PRECONDICIÓN

El método consiste en construir un programa que
requiere para su correcto funcionamiento una precondición
reforzada. La manera más simple de reforzar un aserto s
añadirle conjunciones, y naturalmente no se escogen
arbitrariamente, sino que han de ahorrar camino hacia la
postcondición :requerimos una versión
débil de ésta en la precondición. EN
concreto, el método consiste en debilitar la
postcondición, posiblemente añadiendo
variables ;reforzar la precondición con el aserto
obtenido, posiblemente acompañado de condiciones de
dominio ;añadir los parámetros de
inmersión que sean precisos para que la nueva
precondición tenga sentido, y mantener la
postcondición original.

El debilitamiento proporciona, además, ideas
sobre la programación de la inmersión, y de la
función original en términos de ésta. La
versión débil de la postcondición debe poder
establecerse fácilmente, pues ahora la primera llamada
recursiva está obligada a cumplirla mediante sus
inicializaciones de los parámetros. Por otra parte, el
proceso de debilitamiento marca la diferencia entre la nueva
precondición y la postcondición, luego la
protección del caso directo habrá de permitir
"invertir" este proceso. En los casos recursivos, procuramos
siempre que los únicos parámetros que varíen
de una llamada a la siguiente sean los de inmersión.
Puesto que la postcondición no los menciona, no
habrá diferencia con la de la llamada recursiva, por lo
que no serán necesarias más
operaciones :obtendremos directamente una solución
recursiva final, y una verificación con
postcondición constante.

DEBILITAR ASERTOS

EL método para encontrar un debilitamiento de la
postcondición consiste en hacer aparecer en ella nuevos
parámetros, añadiendo las igualdades que sean
necesarias, y debilitarla luego suprimiendo todas o algunas de
ellas. La primera fase de adición de parámetros
puede ser innecesaria cuando ya se tienen conjunciones, y por
tanto cláusulas que suprimir.

Al escribir el programa, se ha de incorporar a la
cabecera todos los parámetros de
inmersión :tanto los que figuran en el papel de los
resultados, como los que hayamos usado para crear conjunciones a
suprimir. Las conjunciones suprimidas, que indican la diferencia
entre postcondición y precondición, se
convertirán en protecciones del caso directo, y los casos
recursivos presentarán recursividad final.

DEBILITAMIENTO DE LA
POSTCONDICIÓN

Debilitar la postcondición consiste en exigirnos
menos. En su forma más simple, el método consiste
en sustituir la postcondición por un debilitamiento suyo,
manteniendo la precondición. Para debilitar la
postcondición usaremos las técnicas ya descritas, y
con particular frecuencia las que incorporan nuevas variables en
lugar de subexpresiones.

Las igualdades suprimidas no han de olvidarse ;en
este caso, nos indicarán las inicializaciones adecuadas
para recuperar la función original a partir de la
inmersión. En cuanto a la precondición,
posiblemente sea necesario reforzarla con condiciones de dominio
sobre los nuevos parámetros. A veces, no es fácil
predecir cuáles han de ser éstas, pero, si la
verificación y el diseño se realizan
simultáneamente, las propias necesidades de la
verificación nos las proporcionan durante el
desarrollo.

INMERSIÓN DE EFICIENCIA

El principio básico a seguir es : el valor
que se supone que han de tener los nuevos parámetros y
resultados que añadamos ha de constar en la
especificación ; en la precondición si se
trata de parámetros, y en la postcondición si se
trata de resultados. Cada llamada recursiva puede usarlos en
sustitución del valor que consta que tienen, pero
también se compromete a darles el valor que las otras
llamadas recursivas requieran.

TÉCNICA DEL DESPLEGADO Y
PLEGADO

El método de desplegado y plegado permite
obtener, una función recursiva final a partir de una
función recursiva lineal. La recursividad no final se
produce cuando después de la llamada a la función
se han de ejecutar mas instrucciones. Este método consiste
en buscar una inmersión tal que uno de los
parámetros vaya transmitiendo la parte ya calculada del
resultado.

El método sigue los siguientes pasos :para
obtenerla inmersión g, considérese la
expresión que define el caso recursivo de la
función recursiva lineal f a transformar, sea éste
f(x)=c(f(s(x)),x) ;y sustitúyanse en esta
expresión todos los subtérminos que no contengan n
a f ni a c por variables de inmersión. La expresión
resultante define la función inmersora g que deseamos, en
términos de f :g(y, w)=c(f(y),w). La razón
para operar así es que, si el programa para la
función inmersora ha de ser recursivo final, conviene que
la expresión que lo define tenga f(x) como uno de sus
posibles casos particulares , y la solución del caso
recursivo c(f(s(x)),x) como otro posible caso
particular.

Intentaremos obtener el programa mediante simple
sustitución de los casos directos y recursivos de f en la
definición de g. Así, el análisis de casos
de g resultará idéntico al de f.

Los casos directos se obtienen de los de f, al igual que
la función limitadora que garantiza la terminación
y valida la inducción. La sustitución de f por su
valor se denomina desplegado, y la manipulación para
devolver la expresión a la forma requerida
plegado.

OBTENCIÓN DE POSTCONDICIÓN
CONSTANTE

Un programa recursivo final presenta una
verificación con postcondición constante si la
postcondición no depende de los parámetros que
varían de una llamada a la siguiente, es decir, si la
postcondición de la función y la de la llamada
recursiva que genera coinciden. Las variables incluidas en la
postcondición no varían.

Esta condición sólo tiene sentido para la
recursividad final, pues, si el resultado de la llamada recursiva
ya cumple la postcondición que buscamos, podemos
devolverlo sin más tramite.

El proceso de razonamiento que permite obtener una
verificación con postcondición constante para un
programa recursivo final es como sigue :

– Se realiza una inmersión, duplicando aquellos
parámetros que varían de una llamada a la
siguiente, de manera que podamos conservar en todas las llamadas
una copia de sus valores iniciales.

– Como nueva postcondición, requerimos la
antigua, pero aplicada a estos valores iniciales que no
varían, con lo cual obtenemos un programa con
postcondición constante.

– Y para poderlo verificar, reforzamos la
precondición con un aserto que exprese lo
siguiente :que la postcondición sobre los
parámetros variados implica la postcondición sobre
los valores iniciales.

En realidad, por tanto, lo que vamos a proponer es
simplemente una manera de añadir a la precondición
un debilitamiento de la postcondición.

Profundización en programas
iterativos

Intuitivamente, un invariante para un bucle dado es un
aserto que es cierto al comienzo de todas y cada una de las
vueltas del bucle, y que nos permite transmitir
información de la precondición a la
postcondición. Un invariante puede permitir verificar
parcialmente un bucle en el siguiente sentido :si se
demuestra que se cumple antes de entrar en él,
deduciéndolo de la adecuada precondición, la
invariancia garantiza que, cuando el bucle termine, se
seguirá cumpliendo, y de él se puede intentar
deducir la apropiada postcondición.

Esta verificación es parcial, en el sentido de
que demuestra que, si el bucle termina, lo hace cumpliendo la
postcondición ;garantizar la terminación del
bucle requiere un argumento adicional :el decrecimiento de
una función limitadora que toma valor en los naturales.
Ahora, ésta puede depender de las variables que
intervienen en el bucle, ha de estar definida siempre que el
invariante y alguna protección del bucle sean ciertos (al
menos), y su valor ha de decrecer estrictamente a cada vuelta, de
manera análoga a la función que demuestra el
decrecimiento de los parámetros en el correspondiente
programa recursivo final.

Reglas de inferencia.

TRANSFORMACIÓN DE POSTCONDICIÓN
CONSTANTE A ITERATIVO

El invariante del programa iterativo es la
precondición de la función con postcondición
constante.

La función cota es el preorden del programa
recursivo.

Los parámetros de inmersión son las
variables locales de la iteración.

La condición del bucle es la protección
del caso recursivo.

El cuerpo del bucle viene dado por el cambio de los
parámetros.

Después del bucle se ha de implementar el caso
directo del programa recursivo.