Clase de Práctica AED1, 8/6/2000. Demostración de correctitud de ciclos.

 

Ejercicio 2i.

 

Potencia(n:integer,m:integer):integer

 

Especificación de estados

 

P º {n = N₀ Ù m = M₀ Ù (N₀ = 0 Þ M₀ ¹ 0) Ù M₀ ³ 0}

definimos: P_posº { N₀ ¹  0 Ù  M₀ ³ 0 Ù n = N₀ Ù m = M₀ }

Pc º {i = 0 Ù ret_value = 1 Ù P_pos }

B º {i < m}

I º {ret_value = f_potencia n i Ù 0 £ i £ m Ù P_pos }

Fv = m - i

Qc º { ret_value = f_potencia n m Ù i=m  Ù P_pos }

Q º {ret_value = f_potencia N₀ M₀}

 

Código

 

Function Potencia(n:Integer,m:Integer):Integer;

Var

      i:integer;

 

{ P }

if (n<>0) then

i=0;

ret_value:=1;

{ Pc  }

ß

{ I }

while (i<m) do

{ I Ù B }

ret_value:=ret_value*n;

i:=i+1;

{ I }

od;

{ I Ù ~B }

ß

{ Qc }

else

      ret_value:=0;

fi

ß

{Q }

EndFunction;

 

Correctitud del ciclo

 

Es importante demostrar que el ciclo fue especificado y codificado correctamente.

Lo que nos interesa es que partiendo de nuestra precondición del ciclo (Pc), ejecutando una serie de iteraciones podamos alcanzar la postcondición del ciclo (Qc) y que el mismo, en este caso implique la postcondición de la función (ya que luego del ciclo no realizamos ninguna operación más).

 

Para cumplimentar estos requisitos es necesario que el invariante verifique estas propiedades:

 

1. El invariante se cumple en la entrada del ciclo. Esto significa que la precondición del ciclo implique el invariante (PcÞI).
2. El invariante debe cumplirse en cada iteración del ciclo. Tanto en la entrada como en la salida. En el primer caso también debe cumplirse la guarda del ciclo.
3. La función variante es estrictamente decreciente y acotada.
4. Al finalizar el ciclo (no cumplimiento de la guarda) el invariante debe implicar la postcondición del ciclo (I Ù~B Þ Qc). Esto nos asegura que el invariante se acerca paso a paso a la solución del problema.

 

Verifiquemos que si nuestro código cumple con estas propiedades.

 

1. Sabemos que la primera vez  que entramos al ciclo el estado del programa es el indicado por Pc.

Pcº{i = 0 Ù ret_value = 1 Ù P_pos}

 

            siendo nuestro invariante es el siguiente:

           

I º {ret_value = f_potencia n i Ù 0 £ i £ m Ù P_pos }

 

Reemplazando a i por 0 y ret_value por 1 obtenemos:

 

{1 = f_potencia n 0 Ù 0 £ 0 £ m Ù P_pos }  º True

 

ya que n⁰ = 1 (n¹0) por lo que se cumple la primera conjunción, se sigue cumpliendo P_pos ya que no cambiamos el valor de n y m  y por P_pos sabemos que m= M₀ ³ 0 por lo que también se cumple la segunda conjunción.

 

2. Si entramos al ciclo podemos asegurar que i<m.  Supongamos que I se cumple. Demostremos que I se cumplirá a la salida del ciclo.

 

Como  I  y B se cumplen podemos  caracterizar al conjunto de estados posibles con el siguiente predicado.

 

P1º { I  Ù B } º {i<m Ù ret_value = f_potencia n i Ù 0 £ i £ m Ù P_pos }

 

Ahora llamemos i₀ y ret_value₀ a los valores de la variables i y ret_value  en este momento de ejecución.  i₀ y ret_value₀ son un ejemplo de metavariables que son usadas solamente en la descripción de 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 deben ser usadas en las sentencias de un programa.

 

Nuestro predicado anterior puede rescribirse de la siguiente manera:

 

E1 º {i₀<m Ù i=i₀  Ù ret_value = ret_value₀  Ù ret_value₀ = f_potencia n i₀

Ù 0 £ i₀ £ m Ù P_pos }

 

Hasta el momento, solo hemos reescrito de manera conveniente nuestro predicado

I  Ù B. Ahora sigamos paso a paso la ejecución de las sentencias del ciclo.

 

while (i<m) do

E₁ º{i₀<m Ù i=i₀  Ù ret_value = ret_value₀  Ù ret_value₀ = f_potencia n i₀ Ù 0 £ i₀ £ m Ù P_pos }

ret_value:=ret_value*n

E₂ º{i₀<m Ù i=i₀  Ù ret_value = ret_value₀ *n   Ù ret_value₀ = f_potencia n i₀

Ù 0 £ i₀ £ m Ù P_pos }

     º (reemplazando el valor de ret_value₀)

E₂’ º{i₀<m Ù i=i₀  Ù ret_value = f_potencia n i₀ *n   Ù 0 £ i₀ £ m Ù P_pos }

i:=i+1;

E₃  º {i = i₀+1 Ù i₀<m Ù ret_value = f_potencia n i₀*n  i₀ Ù 0 £ i₀ £ m Ù P_pos }

ß?

{ I }

od;

 

Solo nos resta demostrar que E3 Þ I. Pero esto es simple ya que:

 

·        Como  i₀ < m Ù 0 £ i₀ £ m  Þ 0 £ i = i₀+1 £ m

·        ret_value = f_potencia n i₀ *n   = f_potencia n (i₀+1) = f_potencia n i

 

luego se cumple I como queríamos demostrar.

 

3. Debemos probar que la función variante es estrictamente decreciente y acotada inferiormente.

 

La función variante es m-i. Llamemos fv₀=m-i₀ al valor que representa la función variante en una iteración del ciclo.

Luego de ejecutar i:=i+1, fv = m- (i₀+1)= m - i₀- 1= fv₀ –1 por lo que queda demostrado que decrece un paso en cada iteración

Es muy simple ver que está  acotada en 0, ya que m=M₀ para todas las iteraciones y el ciclo incrementa i hasta alcanzar a m.

 

4. Ahora debemos demostrar que (I Ù~B Þ Qc)

 

Sabemos que i³m ya que ha terminado el ciclo y además se cumple el invariante. Por lo tanto nuestro estado está caracterizado por el siguiente predicado

 

{ I  Ù ~B } º {i³m Ù ret_value = f_potencia n i Ù 0 £ i £ m Ù P_pos }

 

Debido a la restricción que impone I sobre i esta necesariamente deberá ser igual a m.

 

{i=m Ù ret_value = f_potencia n i Ù P_pos} º {i=m Ù ret_value = f_potencia n m Ù P_pos }

º

 Qc

 

Ahora veamos que Qc Þ Q:

 

Por P_pos sabemos que n=N₀ y m=M₀ por lo tanto lo reemplazamos y obtenemos

 

{i=m Ù ret_value = f_potencia N₀ M₀ Ù P_pos }

ß

{  ret_value = f_potencia N₀ M₀ } como queríamos demostrar.