Solución del problema 20

 

20. Verificar la corrección parcial de la siguiente función cuyo objetivo es calcular el n-ésimo término de la sucesión de Fibonacci (Fn), teniendo en cuenta que ésta sucesión se define de la siguiente forma:

  • F0 = 0, F1 = 1
  • Fn = Fn-1 + Fn-2
function Fib(n: integer) dev x: integer;
var x0,t,i : integer;
begin
{ n ≥ 0 }
<x0,x> := <0,1>;
for i := 1 to n do
begin
t := x0+x;
x0 := x;
x := t
end
{ x = Fn }
end

Reescribimos el programa cambiando el bucle for por su equivalente while e indicamos los puntos donde iran los asertos (el invariante estará en el punto 1):

function Fib(n: integer) dev x: integer;
var x0,t,i : integer;
begin
{ n ≥ 0 }
<x0,x,i> := <0,1,1>;
••• (1)-0 •••
while i <= n do
begin
••• (2)-n •••
t := x0+x;
••• (3)-n •••
x0 := x;
••• (4)-n •••
x := t
••• (5)-n •••
i := i+1
••• (1)-n •••
end
••• (6) ••• { x = Fn }
end

En este problema nos dan la postcondión deseada y partiendo de ella podemos proponer un candidato a invariante: Si observamos el código, vemos que el bucle va calculando términos de la sucesión aplicando la fórmula, y que al terminar el bucle se tiene que i = n+1. Para obtener la postcondición, en la última iteración es necesario que x = Fi-1, para que al salir del bucle y hacer la sustitución obtengamos x = Fn. Además, se puede apreciar que x0 almacena el término anterior, por lo que añadimos x0 = Fi-2 al candidato a invariante (Nota: Se debe incluir la condición i > 1 para que el término Fi-2 tenga sentido).

Iteramos para comprobar que el candidato a invariante no cambia en cada iteración:

Hemos comprobado que nuestro candidato a invariante es constante en cada iteración y además proporciona la postcondición deseada. Ha sido necesario añadir la condición i ≤ n+1 para que al salir del bucle podamos decir que i = n+1, pero esto no afecta a la demostración.

Falta comprobar que la precondición del bucle implica al candidato a invariante:

Ouch! La comprobación ha fallado! El invariante exige que i sea mayor que 1 y al comienzo del bucle vale precisamente 1. Tampoco se pueden reconciliar los términos almacenados en x y x0. De hecho, basta ejecutar el algoritmo para ver que realmente el resultado no es Fn.

Respuesta: La verificación del algoritmo no puede demostrar que se cumpla la postcondición indicada en el problema.

¿Y que es lo que hace realmente este algoritmo? Si realizamos un par de iteraciones encontramos facilmente cual es el verdadero invariante y la verdadera postcondición de la función:

CESAR VACA RODRIGUEZ
cvaca@infor.uva.es