|
18. Verificar la corrección total de la siguiente función: function potencia(a: real; b: integer) dev p: real;
var i: integer;
begin
{ b ≥ 0 }
<p,i> := <1,b>;
while i > 0 do <p,i> := <p*a,i-1>
end;
|
Reescribimos el programa para indicar los puntos donde iran los asertos (el invariante estará en el punto 1):
Realizamos varias iteraciones, hasta que veamos un candidato a invariante:
|
Se puede ver claramente cómo cambia el aserto (1) en cada iteración. Proponemos un candidato a invariante y lo verificamos:
 |
Falta comprobar que la precondición antes de entrar en el bucle (aserto (1)-0) implica al invariante:
 |
Ya hemos demostrado la corrección parcial, y se ha obtenido una postcondición que indica que la función calcula la potencia de un número real elevado a un exponente entero positivo. Queda demostrar la finitud:
Mirando la condición del bucle podemos proponer como función de cota el valor de la variable i:
 |
Donde k representa el número de iteraciones. Expresamos la cota en función de k (basta observar que i es igual a b antes de entrar en el bucle y que decrece en cada iteración) y comprobamos que decrece en cada iteración:
 |