Algoritmos y Estructuras de Datos I

Facultad de Ciencias Exactas y Naturales

Universidad de Buenos Aires

Primer Cuatrimestre de 2000

Apunte de Programación Imperativa

Escribir la siguiente funcion con sus respectivas precondiciones y postcondiciones. Escribir los invariantes y los variantes en los casos en los cuales incluyan ciclos.

Producto (n: integer, m: integer) : integer (sin usar *)

Aridad de la función Producto:

function Producto (n: integer, m: integer) : integer

Precondición y Poscondición:

P º { n = N₀ Ù m = M₀ }

Es decir, las variables n y m son parámetros de entrada de la función Producto, y llamamos N₀ y M₀ a sus respectivos valores iniciales

Q º { ret_value = N₀ * M₀ }

O sea, la función retorna la multiplicación de los valores de los parámetros de entrada.

Algoritmo:

El algoritmo que usaremos consiste en sumar |n| veces m en ret_value. Después, dependiendo del signo de n, se se cambia el signo de ret_value. Tal como la intuición nos indica, las estructuras de control necesarias para estas dos etapas son un ciclo (while) y un condicional (if), respectivamente.

Estados de antes y después del ciclo:

Utilizaremos a j para iterar |n| veces.

Pc º { ret_value = 0 Ù j = Abs n Ù P}

Queremos llegar, una vez terminado el ciclo, a este estado:

Qc º { ret_value = (Abs n) * m Ù j = 0 Ù P }

Invariante del ciclo:

I º { 0 £ j £ Abs n Ù ret_value = ((Abs n) - j) * m Ù P }

Guarda del ciclo:

B º { j > 0 }

Función variante del ciclo:

La función variante debe ser estrictamente decreciente, y debe estar acotada inferiormente. En este caso, notemos que j cumple esas dos condiciones. Entonces:

FV = j

No en todos los casos la función variante es tan trivial. Muchas veces hay que rebuscárselas un poco para encontrarla.

Código

function Producto (n: integer, m: integer) : integer

var j: integer := Abs(n);

ret_value:=0;

while (j > 0) do

ret_value:= ret_value + m;

j := j - 1;

od;

if (n < 0)

then ret_value := - ret_value;

else skip;

fi;

endfunction

Correctitud del Ciclo:

Veamos que se cumple el teorema del invariante:

1) (Pc ÞI). El invariante se cumple al entrar al ciclo por primera vez.

Sabemos que al entrar al ciclo por primera vez, ret_value vale 0, j vale Abs n y los valores de n y m no fueron modificados. Es fácil comprobar, haciendo los reemplazos correspondientes, que esta valuación hace verdadero al invariante del ciclo.

2) (I Ù B) { S } I. El invariante se cumple en cada iteración del ciclo.

Supongamos que el invariante se cumple al entrar al ciclo en alguna iteración. Queremos ver que al terminar la ejecución de esa iteración, el invariante se seguirá cumpliendo.

Como, en efecto, entramos al ciclo, podemos asegurar que j > 0 (de otro modo, no habríamos entrado). Además, dijimos que suponemos que el invariante se cumple. Entonces, podemos afirmar que:

E_{ciclo_1} º { j > 0 Ù 0 £ j £ Abs n Ù ret_value = ((Abs n) - j) * m Ù P }

Estamos diciendo que j es mayor que 0, y mayor o igual a 0. Claramente, la segunda afirmación es redundante. Entonces, este predicado puede reescribirse de la siguiente manera:

E_{ciclo_1}' º{ 1 £ j £ Abs n Ù ret_value = ((Abs n) - j) * m Ù P }

Ahora, llamemos J₀ al valor de la variable j en este momento de la ejecución. Del mismo modo, llamemos R₀ al valor de la variable ret_value en este momento. J₀ y R₀ son ejemplos de metavariables, que usamos solamente en la descripción de los estados, para referirnos al valor de las variables en algún momento de la ejecución. Debe quedar claro que las metavariables bajo ninguna circunstancia pueden ser usadas en las sentencias de un programa.

Entonces, el predicado anterior puede reescribirse del siguiente modo:

E_{ciclo_1}'' º { 1 £ J₀ £ Abs n Ù R₀ = ((Abs n) - J₀) * m Ù j = J₀ Ù ret_value = R₀ Ù P }

Hasta ahora, solamente hemos reescrito de manera conveniente el estado original B Ù I, sin agregar ni quitar información sobre las variables del programa. Sigamos ahora paso a paso la ejecución del interior del ciclo, a partir de ese estado:

while (j > 0) do

E_{ciclo_1}'' º { 1 £ J₀ £ Abs n Ù R₀ = ((Abs n) - J₀) * m Ù j = J₀ Ù ret_value = R₀ Ù P }

ret_value := ret_value + m;

E_{ciclo_2} º { 1 £ J₀ £ Abs n Ù R₀ = ((Abs n) - J₀) * m Ù j = J₀ Ù ret_value = R₀ + m Ù P }

j := j - 1;

E_{ciclo_3} º{ 1 £ J₀ £ Abs n Ù R₀ = ((Abs n) - J₀) * m Ù j = J₀ - 1 Ù ret_value = R₀ + m Ù P }

od;

Entonces, como dijimos antes, tenemos que verificar si el último estado respeta lo descripto por el invariante del ciclo.

En primer lugar:

j = J₀ - 1 entonces J₀ = j + 1

1 £ J₀ £ Abs n Ù J₀ = j + 1 entonces 1 £ j + 1 £ Abs n entonces 0 £ j £ (Abs n) - 1, lo cual respeta la primera parte del invariante.

En otras palabras, esto nos está diciendo que, si suponemos que j tenía un valor entre 0 y Abs n al entrar a una iteración del ciclo, entonces al terminar dicha iteración, va a tener un valor entre 0 y (Abs n) - 1, lo cual respeta el invariante.

Por otro lado:

ret_value = R₀ + m entonces R₀ = ret_value - m

R₀ = ((Abs n) - J₀) * m Ù J₀ = j + 1 Ù R₀ = ret_value - m entonces ret_value - m = ((Abs n) - (j + 1)) * m

entonces ret_value = ((Abs n) - j - 1) * m + m entonces ret_value = ((Abs n) - j) * m.

¡Y esto es exactamente lo que dice la segunda parte del invariante del ciclo!

Es decir, si al entrar a una iteración del ciclo ret_value vale ((Abs n) - j) * m, al salir de dicha iteración seguirá respetando esa relación de valores, respecto al nuevo valor de j.

Entonces, acabamos de demostrar que, suponiendo que el invariante se cumple al entrar a una iteración del ciclo, después de ejecutar las sentencias del interior del ciclo, el invariante se seguirá cumpliendo.

3) ( I Ù B Ù fv =T ) {S} ( I Ù fv < T ). La función variante es estrictamente decreciente.

De la misma forma que en la demostración anterior, supongamos que se cumple y I Ù B.

Llamamos J₀ al valor de j y fv= fv₀. Luego fv₀ = J₀.

Al ejecutar j:=j-1 tenemos que fv = (J₀-1) = fv₀ -1 < fv₀  por lo que queda demostrado que fv decrece en cada iteración.

4) (fv = cota Þ ~B). Cuando la función variante alcanza su cota inferior la guarda se hace falsa.

En este caso la demostración es trivial ya que la cota inferior de fv es 0 y alcanza este valor cuando j es 0.

La condición en B es j>0 por lo que cuando j llega a 0 la condición deja de cumplirse.

5) (I Ù ~B Þ Qc). Al terminar el ciclo se respeta el estado Qc

Sabemos que j £ 0 —porque si no, el ciclo no habría terminado—, y además que el invariante se cumple —gracias a los dos puntos anteriores—. Entonces:

I Ù ~B º{ j £ 0 Ù 0 £ j £ Abs n Ù ret_value = ((Abs n) - j) * m Ù P}

Observemos que j no puede tomar un valor que no sea 0. Entonces, este predicado se puede reescribir así:

{ j = 0 Ù ret_value = (Abs n) * m Ù P }

Este estado respeta a Qc —es más, son exactamente iguales—.

Antes de seguir, notemos que la variable j ya no figura más en el código ni en la postcondición de la función. Entonces, podemos "olvidarnos" de ella, ya que no tiene influencia en los siguientes estados.

Qc º{ j = 0 Ù ret_value = (Abs n) * m Ù P } Þ Q'c º{ ret_value = (Abs n) * m Ù P }

Continuemos, ahora sí, la ejecución de las últimas líneas de código, a partir del estado Q'c.

Si en el if-fi que sigue se entra por la rama del then, es porque n es menor que 0. En ese caso, Abs n = - n, por lo que habrá que negar el resultado obtenido. Si se entra por la rama del else, es porque n es mayor o igual que 0, en cuyo caso Abs n = n.

{ ret_value = (Abs n) * m }

if (n < 0)

then { ret_value = (Abs n) * m Ù n < 0 } º { ret_value = (-n) * m Ù n < 0 Ù P }

res := -res

{ ret_value = n * m Ù n < 0 Ù P }

else { ret_value = (Abs n)*m Ù n ³ 0 Ù P } º { ret_value = n * m Ù n ³ 0 Ù P}

skip

{ ret_value = n * m Ù n ³ 0 Ù P }

fi;

Ahora, el estado de las variables después de este if-fi es la disyunción de los postcondiciones de las ramas:

{ (ret_value = n * m Ù n < 0 Ù P) ú (ret_value = n * m Ù n ³ 0 Ù P) }

º { ret_value = n * m Ù (n < 0 ú n ³ 0) Ù P } º { ret_value = n * m Ù P }ºQ'

Llegamos así a la postcondición del algoritmo, que dice que ret_value tiene el valor del producto entre n y m, ya que claramente Q' Þ Q pues P indica que n=N₀ y m=M₀.

De esta manera, hemos demostrado que el algoritmo elegido nos sirve para llegar desde la precondición hasta la postcondición del mismo. En otras palabras, la función hace lo que queríamos: devolver el producto de dos números enteros.