Diseño Iterativo

Vista previa del material en texto

Diseño Iterativo
 
INTRODUCCIÓN 
 
En este tema vamos a volver al tipo de algoritmo secuencial sin recursividad, al que estábamos acostumbrados en Programación I (en este tema los llamaremos algoritmos iterativos, porque contienen bucles). Hasta ahora hemos aprendido varias cosas sobre este tipo de programas: 
 
· - cómo se calcula su eficiencia (tema 1). 
 
· - cómo obtener un algoritmo iterativo a partir de uno recursivo. 
 
En este tema vamos a centrarnos en tres ideas: 
 
· - cómo se verifica que un algoritmo secuencial/iterativo es correcto. 
 
· - cuáles son los puntos esenciales para la comprobación de que un algoritmo iterativo es correcto (basándonos en el concepto de INVARIANTE) y en lo aprendido en la idea anterior. 
 
· - cómo se obtiene (deriva) un algoritmo iterativo a partir de una especificación formal. 
 
 
 
DISEÑO ITERATIVO 
 
Lenguaje imperativo: secuencias de órdenes. 
 
Los estados por los que pasa la ejecución de un programa, dado un estado inicial, está determinada. 
 
La especificación de un algoritmo, como sabemos, viene dada por dos predicados: 
 
PRECONDICIÓN: conjunto de estados válidos al comienzo del algoritmo. 
 
POSTCONDICIÓN: conjunto de estados alcanzables a su terminación. 
 
Para verificar un algoritmo iterativo, vamos a fijarnos en los estados intermedios (entre instrucciones). 
 
ASERCIÓN o ASERTO: conjunto de estados alcanzados por un algoritmo en un punto intermedio de su ejecución. Cada uno de ellos representa una afirmación sobre una propiedad que se satisface siempre que el control del programa pasa por el punto donde está situado el mismo. 
 
 
Escribiendo un aserto entre cada dos instrucciones elementales del algoritmo obtenemos una forma de razonar sobre la corrección de un programa imperativo. 
 
S = s1;s2;s3;...sn 
 
{ Q ≡ P0 } s1 { P1 };...;{ Pn-1 } sn { Pn ≡ R } 
 
Si el aserto inicial Q se satisface, y cada “programa” elemental si , consistente en una sola instrucción satisface { Pi-1 } si { Pi }, entonces se satisface finalmente la postcondición R y el programa es correcto. 
 
Reglas para decidir si una instrucción elemental s satisface una especificación dada {Q} s {R}. 
 
Formato a emplear: 
 
	E1,....,En 
------------- 
E1’....,Em’ 
 
que significa: de la veracidad de las expresiones E1,....,En se infiere la veracidad de las expresiones E1’....,Em’ 
 
Cuando a partir de una instrucción y el aserto que aparece después de ella, nos piden calcular el aserto que debe ir antes de ella, a este predicado se le llama “pmd” o precondición más débil. 
 
Vamos a ir calculando, a partir de la postcondición, la precondición más débil de cada uno de las instrucciones del programa, desde la última instrucción hasta la primera. Cada pmd calculada la tomaremos como postcondición de la instrucción anterior, y así sucesivamente hasta el comienzo del programa. La pmd que obtengamos de este proceso será la pmd del programa. Si la precondición que teníamos (Q) cumple Q => pmd (S, R), siendo S el algoritmo y R su postcondición, el algoritmo realizado es correcto. 
 
Todas las definiciones que vamos a ver respetan unas normas generales: 
 
1.- Una precondición siempre puede ser reforzada 
 
	{Q} S {R}, Q’ 	 Q 
---------------------- {Q’} S {R} 
 
 
 
 
 
2.- Una postcondición siempre puede ser debilitada 
 
	{Q} S {R}, R 	 R’ 
---------------------- {Q} S {R’} 
 
 
3.- Las precondiciones admisibles para un algoritmo pueden componerse mediante las conectivas ∧ y ∨, siempre que se haga lo mismo con las respectivas postcondiciones. 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
{
Q
1
}
 
S
 
{
R
1
}
,
 
{
Q
2
}
 
S
 
{
R
2
}
 
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
 
{
Q
1
 
∧
 
Q
2
}
 
S
 
{
R
1
 
∧
 
R
2
}
,
 
{
Q
1
 
∨
 
Q
2
}
 
S
 
{
R
1
 
∨
 
R
2
}
 
 
 
INSTRUCCIÓN “nada” 
 
La instrucción nada tiene como efecto el no hacer ninguna acción 
 
 
 
	---------------------------- 
{Q} nada {Q} 
 
 
INSTRUCCIÓN “abortar” 
 
Esta instrucción impide que se alcance cualquier estado útil 
 
	 
------------------------------- {falso} abortar {Q} 
 
 
No existe ningún estado de partida que garantice que la instrucción abo rtar termina en un estado definido. 
 
INSTRUCCIÓN de asignación 
 
Esta instrucción x := E tiene como efecto que la expresión E sea evalua da en el estado en curso y su valor sea asignado a la variable x, que pierde su antiguo valor 
 
	 
---------------------------------- { Dom (E) ∧ REx} x::= E {R} 
 
Esta regla permite obtener una precondición admisible a partir de la postcondición deseada para la instrucción. 
 
El predicado REx se construye sustituyendo en R todas las apariciones libres de x por la expresión E. Por su parte, Dom(E) es el conjunto de todos los estados en los que la expresión E está definida. 
 
Cuando trabajamos con asignaciones múltiples ( la asignación de una lista de expresiones a una lista de variables), utilizamos la notación 
 
<x1,...,xn> := <E1,...,En> 
 
siendo cada expresión Ei del mismo tipo que la variable xi y todas las xi variables distintas. 
 
El significado es que primero se evalúan en el estado en curso todas las expresiones Ei. A continuación, se asignan los valores obtenidos a sus correspondientes variables, que pierden sus valores anteriores. 
 
 
	 
------------------------------------------------------------ { RE1,E2,...,Enx1,x2,...xn} <x1,...,xn> := <E1,...,En> {R} 
 
 
COMPOSICIÓN SECUENCIAL DE INSTRUCCIONES 
 
 
	{ Q } S1 { P } , { P } S2 { R} ------------------------------- 
{ Q } S1 ; S2 { R } 
 
 
COMPOSICIÓN CONDICIONAL DE INSTRUCCIONES 
 
(simple) Si B entonces S1 si no S2 fsi 
 
 
	{ Q ∧ B } S1 { R } , { Q ∧ B } S2 { R} 
-------------------------------------------------------------------- 
{ Q ∧ Dom(B) } Si B entonces S1 si no S2 fsi { R } 
 
 
(múltiple) Caso B1 → S1 ... Bn → Sn fcaso 
 
	{ Q ∧ B1 } S1 { R } ,... ,{ Q ∧ Bn} Sn { R} 
----------------------------------------------------------------------------------- 
{ Q ∧ UNA (B1,...,Bn)} caso B1 → S1 ... Bn → Sn fcaso { R } 
donde UNA (B1,...,Bn) ≡ (∧ i ∈ {i..n} Dom (bi)) ∧ (N i ∈ {i..n}. Bi) = 1 
 
INSTRUCCIONES ITERATIVAS. INVARIANTES 
 
mientras B hacer S fmientras 
 
INVARIANTE predicado que describe todos los estados por los que atraviesa el cómputo realizado por el bucle, observados justo antes de evaluar la condición B de terminación. 
 
Se denomina así porque se satisface antes y después de cada iteración E. 
 
Si el bucle termina, lo hace satisfaciendo el invariante P, y, además, la negación de la condición B. La postcondición del bucle será pues, P ∧ B 
 
El invariante P es a la vez precondición y postcondición del cuerpo S de la iteración, ya que ésta modifica el estado pero no las relaciones entre las variables. Además, Dom (B) ha de cumplirse cada vez que la condición B va a ser evaluada, es decir, ha de satisfacerse P Dom(B). 
 
También debemos encontrar una función (llamada función limitadora) t: estado→ Z que se mantenga no negativa cada vez que se va a ejecutar el cuerpo S y que decrezca cada vez que se ejecuta éste. 
 
Para obtener esta función debemos observar las variables que son modificadas por el cuerpo S del bucle y construir con (algunas de) ellas una expresión entera t que decrezca. Después se ajusta t, si es necesario, para garantizar que se mantiene no negativa siempre que se cumple P ∧ B. 
 
Se debe satisfacer: 
 
1.- P ∧ B 	 t ≥ 0 
 
2.- { P ∧ B ∧ t = T} S { t < T}, para cualquier constante entera T. 
 
 
	P 	 Dom (B), {P ∧ B} S{P}, P ∧ B 	 t ≥ 0, { P ∧ B ∧ t = T} S { t < T} 
---------------------------------------------------------------------------------------- 
{P} mientras B hacer S fmientras {P ∧ B} 
 
 
El invariante debe ser lo suficientemente fuerte para poder deducir la postcondición después. 
 
El invariante debe ser lo suficientemente simplepara no restringir el dominio. 
 
Los bucles “repetir” y “para” se verificarán a partir de la forma equivalente “mientras” correspondiente. 
 
 
 
VERIFICACIÓN A POSTERIORI de UN PROGRAMA IMPERATIVO 
 
Vamos a trabajar con pequeños programas ya construidos. 
 
El esquema de programa con el que vamos a trabajar es: 
 
	{Q} 
Inic; 
Mientras B hacer {P} 
S; 
Fmientras 
{R} 
 
Utilizamos este tipo de programas por su generalidad y porque cualquier programa imperativo puede descomponerse en pequeños algoritmos que respondan a este esquema (si hay varios bucles en secuencia, se inventan predicados intermedios, y si hay varios bucles anidados, se comienza verificando el más interior) 
 
Reglas a aplicar: 
 
0.- “Inventar” un invariante P y una función limitadora t. Comprobar que P => Dom (B). 
 
Pueden existir muchos predicados invariantes de un bucle. El que se necesita ha de ser: 
 
· - lo suficientemente fuerte para que, junto con B, conduzca a la postcondición R. 
 
· - lo suficientemente débil para que las instrucciones de inicialización hagan que se satisfaga antes de la primera iteración y el cuerpo S del bucle lo mantenga invariante. 
 
 
Para hallar el invariante, se puede comenzar tabulando para unas cuantas iteraciones los valores de las variables modificadas por el bucle. 
 
 
Comprobar: 
 
1.- P ∧ B => R 
2.- { Q } Inic { P } 
3.- { P ∧ B } S { P } 
4.- P ∧ B => t ≥ 0 
5.- { P ∧ B ∧ t = T } S { t < T } 
 
 
 
{
Q
≡
 
 
n
 
≥
 
0
}
 
	mientras i n hacer	} 
s := s + v[i]; 
i := i + 1; 
fmientras 
ffun 
{ R ≡ s = α ∈ {1 ..n}. v [α] } 
 
0.- Inventamos un invariante para el problema y una función limitadora 
 
Realizamos una tabulación con los valores de las variables en el bucle para ver cuál es la relación que guardan 
 
	i 
	s 
	1 
	0 
	2 
	v[1] 
	3 
	v[1] + v[2] 
	4 
	v[1] + v[2] + v[3] 
	5 
	v[1] + v[2] + v[3] + v[4] 
 
Como se debe cumplir, además P ∧ B => R, escogemos como invariante (por el momento) P ≡ 1 ≤ i ≤ n+1 ∧ s = Σ α ∈{1..i-1}v[α]. Hay que comprobar que 
 
P => Dom (B) 
1 ≤ i ≤ n+1 ∧ s = Σ α ∈{1..i-1}v[α] => Dom (i ≤ n) 
 
Como función limitadora elegimos t = n – i, ya que es una expresión en función de s y de i que se mantiene no negativa y que decrece en cada vuelta del bucle. 
 
Vamos a comprobar los 5 puntos de la verificación. 
 
 
1.- P ∧ B => R 
 
(1 ≤ i ≤ n+1 ∧ s = Σ α ∈{1..i-1}v[α] ) ∧ i > n => s = Σ α ∈{1..n}v[α] cierto 
 
 
2.- { Q } Inic { P } 
 
Verificaremos el siguiente trozo de programa: 
{Q≡ n ≥ 0} 
<s,i> := <0,1> 
{P≡ 1 ≤ i ≤ n+1 ∧ s = Σ α ∈{1..i-1}v[α]} 
 
pmd (P, ins) = precondición más débil de la ejecución de ins con postcondición R. 
 
Q => pmd (P, <s,i> := <0,1>) 
Q => P s,i 0,1 
Q => (1 ≤ 1 ≤ n+1 ∧ 0 = Σ α ∈{1..0}.v[α] ) Q => 0 ≤ n n ≥ 0 => 0 ≤ n cierto 
 
 
3.- { P ∧ B } S { P } 
 
Verificaremos el siguiente trozo de programa: 
DERIVACIÓN FORMAL DE PROGRAMAS IMPERATIVOS 
 
Programación “dirigida por objetivos”: tenemos la postcondición y vamos a hacer nuestro programa en función de ella. 
 
La técnica incluye: 
 
· - Derivación de instrucciones simples 
 
· - Derivación de bucles: 
 
1.- Precisar la especificación (Sobre todo, la postcondición) 
 
2.- Derivar el invariante a partir de la postcondición. 
 
3.- Derivar cada parte del programa (condición de terminación, inicializaciones y cuerpo del bucle), a partir del invariante. 
 
El tipo de programas con el que vamos a trabajar es: 
 
	{Q} 
Inic; 
Mientras B hacer {P} 
S; 
Fmientras 
{R} 
 
 
DERIVACIÓN DE INSTRUCCIONES SIMPLES 
 
Cuando no necesitamos bucles, podemos deducir instrucciones simples de un modo semiformal, partiendo siempre de la postcondición R que deseamos para cada instrucción. 
 
· - Si la postcondición R incluye igualdades de la forma x = E, siendo E una expresion, se ensayarán en primer lugar instrucciones de asignación de la forma x := E, que traten de establecer dichas igualdades. 
 
· - Para cada instrucción de asignación se calculará la precondición 
 
Dom(E) ∧ R Ex 
 
suficiente para que dicha asignación establezca R. 
 
 
· - Si la precondición Q de la instrucción garantiza Dom(E) ∧ R Ex , la asignación x := E es todo lo que necesitamos. 
 
· - Si no es así, se analiza qué condición adicional Bx se necesita para que Q ∧ Bx R. Si la disyunción de todas las condiciones Bx para las distintas instrucciones de asignación ensayadas es implicada por Q, entonces una instrucción condicional de la forma 
 
caso B1 -> x1 := E1 ... Bn -> xn := En fcaso 
 
 es lo que necesitamos para establecer R. 
 
 
 
DERIVACIÓN DEL INVARIANTE A PARTIR DE LA POSTCONDICIÓN 
 
Son técnicas aproximadas, no hay un método “fijo”. 
 
Una de las técnicas consiste en ver el invariante como un predicado cuya componente principal es un predicado más débil que la postcondición. 
 
Técnicas para debilitar un predicado: 
 
· - Eliminar una conjunción. Si R es de la forma R1 ∧ R2, una de las dos conjunciones ( la que sea más fácil de establecer al comienzo del bucle, se tomará como P. La otra será directamente B, de forma que P ∧ B conducen obviamente a R. 
 
· - Incorporar una variable. Si en R sustituimos cierta expresión φ(x), donde x representa el conjunto de variables que intervienen en el bucle, por una variable nueva w, obtenemos un nuevo predicado P(x,w), que satisface la siguiente implicación 
 
 
P(x,w) ∧ (w = φ(x)) 	 R 
 
Tomaremos P como invariante y w = φ(x) como condición de terminación B. 
 
 
DERIVACIÓN DE BUCLES A PARTIR DE INVARIANTES 
 
· - Conociendo el invariante P y la postcondición R del bucle, determinar cuál ha de ser B de forma que se satisfaga P ∧ B 	 R. A partir de B, obtener B. 
 
· - Conociendo P, determinar unas instrucciones de inicialización Inic, lo más simples posibles ( normalmente asignaciones), que establezcan P al comienzo del bucle y que satisfagan {Q} Inic {P}. En este proceso pueden ser necesarios algunos ajustes a la precondición Q. 
 
 
· - Hasta el momento, tenemos 
 
	{Q} 
Inic; 
Mientras B hacer {P} 
¿? 
Fmientras 
{R} 
 
Ahora debemos derivar el cuerpo S del bucle, para lo cual seguiremos los siguientes pasos: 
 
a) a) Incluimos, al final de S, una instrucción avanzar, que haga progresar el bucle hacia su terminación. (conocemos el valor inicial de las variables y la condición B) que hace terminar el bucle. También se conoce la estrategia general de diseño del bucle, con lo que no es difícil conjeturar una función limitadora t. La instrucción avanzar ha de hacer decrecer t. 
 
b) b) Para restablecer la invariancia que incluye la instrucción avanzar, debemos incluir otras instrucciones que restablezcan dicha invariancia, ya que ha de cumplirse { P ∧ B } S { P }. Las llamaremos restablecer. El cuerpo del bucle va a quedar: 
 
 
	Mientras B hacer {P} 
{P ∧ B} restablecer; avanzar; 
{R} 
Fmientras 
 	1 
 	1 
 	15 
image1.png
image2.png