Prii 2009 2010

UNED 2009-2010

Práctica de Programación 2

Especificación del problema y diseño del algoritmo recursivo



fun trans(m: vector[1..F,1..C] de bool; Hf, Hc, Xf, Xc: nat; If, Ic: ent) dev (b:bool)
caso
| |
fcaso
ffun




Validación de la recursividad


1) Completitud de la alternativa

Verificar:




2) Satisfacción de la precondición para la llamadainterna

Verificar:

Voy a verificarlo para el caso


De la precondición asumo como cierto que y de la precondición con la llamada sucesora puedo probar que si entonces y por tantoqueda comprobado que

Se puede verificar de forma similar para los demás casos:

o

o

o

3) Base de la inducción

Verificar:

En el caso trivial, los valores de Hf = Xf y Hc= Xc.



Esto es, el caso trivial.


4) Paso de inducción

Verificar:

Al tratarse del caso no trivial, voy a asumir que



5) Definición de estructura de Preorden Bien FundadoVerificar:

La función de cota escogida es la distancia a recorrer:
Al tratarse de números naturales, se valida que siempre será

6) El tamaño de los subproblemas decrece estrictamente.Verificar:

Al tratarse del caso no trivial, voy a asumir que



Siendo la demostración equivalente para los demás casos.

Paso a recursividad finalSustituiremos por la variable w.

Desplegado



Siendo la operación AND (^) la función combinatoria, el resultado de aplicar la equivalenciaanterior en el diseño del algoritmo recursivo es:


caso
| |
fcaso


caso
| |
fcaso

Plegado

El nuevo parámetro de la nueva función g (o itrans) seráfun itrans(m: vector[1..F,1..C] de bool; Hf, Hc, Xf, Xc: nat; If, Ic: ent; w: bool) dev (b: bool)
caso
| |
fcaso
ffun


Transformación a iterativa




Implementación...