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.