Solución del problema 33

 

33. Verificar la corrección parcial de la siguiente función, cuyo objetivo es evaluar mediante el método de Horner el polinomio an·xn + an-1·xn-1 + ··· + a1·x + a0 para un determinado valor de x:

const N = ..;

function Horner(v: array[0..N] of real; x: real) dev r: real;
var i : integer;
begin
{ N ≥ 0 }
r := 0;
for i := N downto 0 do
r := v[i]+r*x;
{ r = α : 0 ≤ α ≤ N : vα·xα }
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 Horner(v: array[0..N] of real; x: real) dev r: real;
var i : integer;
begin
{ N ≥ 0 }
<r,i> := <0,N>;
••• (1)-0 •••
while i >= 0 do
begin
••• (2)-n •••
r := v[i]+r*x;
••• (3)-n •••
i := i-1;
••• (1)-n •••
end
••• (4) ••• { r = α : 0 ≤ α ≤ N : vα·xα }
end;

Aunque en este problema nos dan la postcondión deseada y partiendo de ella podrímos proponer un candidato a invariante, resulta más sencillo en este caso realizar varias iteraciones y observar el resultado:

Podemos apreciar que la variable r almacena un polinomio en el que intervienen las variables desde vN hasta vi+1. Calculando el modo en que varían las potencias podemos sugerir (e iterar) el siguiente candidato a invariante:

Se comprueba que el invariante no cambia y además proporciona la postcondición deseada. Por último, se verifica que la precondición del bucle implica al invariante:

CESAR VACA RODRIGUEZ
cvaca@infor.uva.es