Derivación de programas

-- Introducción --

La derivación de un programa es un proceso que permite construir las instrucciones que lo

componen a partir de especificación formal, partiendo de la postcondición que describe el
estado de programa que se desea alcanzar.

Se presentan los métodos de derivación de algoritmos iterativos a partir de la especificación,

con especial atención a la derivación de bucles a partir del invariante.

En la tripleta de Hoare:

{ Q } S { R } : S será desconocido.

Luego, se usa la especificación pre/post para diseñar programas.

Contenido

1 Derivación de programas iterativos

1.1 Asignación
 1.2 Composición secuencial
 1.3 Composición alternativa
 1.4 Composición iterativa
2 Ejemplo

Derivación de algoritmos iterativos

Una vez que hemos estudiado las técnicas para verificar la corrección de programas vamos
a estudiar las técnicas que permiten diseñar programas a partir de la especificación.

Enfoque: Usar las reglas de verificación para diseñar programas, de forma que para los
programas obtenidos ya esté demostrada su corrección.

Descomponer la tarea de la programación en distintas subtareas, de forma

que nos podemos concentrar en distintos aspectos del proceso de diseño del
programa.
Método de derivación
Se trata de derivar un programa que cumpla la especificación { Q } S { R }

Es decir, hay que decidir cuál de las estructuras disponibles en el lenguaje

algorítmico es la que corresponde a la acción S:

 Asignación
 Composición secuencial
 Composición alternativa
 Composición iterativa

Asignación
Cuando no son necesarios bucles la deducción de instrucciones simples puede hacerse de
un modo semiformal, partiendo de la postcondición R que deseamos para cada instrucción:

 Si la postcondición R incluye igualdades de la forma x=E siendo E una expresión

Ent se "ensayarán" en primer lugar instrucciones de asignación de la forma x=E
que traten de establecer dichas igualdades.

 Luego se debe hallar R  pmd(S, R)

 El caso más habitual es cuando la única diferencia entre la postcondición y la

precondición es una igualdad de la forma x = E donde E es una expresión que se
puede obtener mediante operaciones predefinidas o especificadas.

Composición secuencial
 Para cada instrucción de asignación se debe calcular la precondición REx suficiente
para que dicha asignación establezca R.

 Si la precondición Q de la instrucción garantiza REx la asignación es todo lo que se

necesita.
  Si la postcondición R incluye igualdades de la forma x = E se ensayarán en primer
lugar instrucciones de asignación de la forma x = E que traten de establecer dichas
igualdades.

 Para cada instrucción de asignación se calculará la precondición REx suficiente para

que dicha asignación establezca R. Luego, en este caso se parte de la postcondición
R que se desea para cada instrucción

Usamos esta opción cuando decidimos que para obtener la postcondición R es necesario
obtener un aserto intermedio T, que nos acerca a R. En ese caso, la derivación de S se
transforma en la derivación de dos acciones S1 y S2 que cumplan

{ Q } S1 { T } y
{ T } S2 { R }

Composición alternativa
Usamos esta opción cuando decidimos que los datos de entrada no admiten un tratamiento
uniforme para obtener la postcondición.

 Se deben encontrar condiciones B1, …, Bn de tal forma que se cumpla

Q  B1 v B2 v … v Bn

Luego, para cada condición Bi deberemos derivar las acciones Si que verifiquen

{ Q ʌ Bi } Si { R } para i= 1, …, n

Y así, el algoritmo resultante será de la forma:

S = si B1  S1 … Bn  Sn fin-si

Composición iterativa
Esta opción se usa cuando decidimos que la postcondición debe obtenerse repitiendo
una determinada acción.

Para obtener el algoritmo utilizamos el método de derivación de bucles a partir del

invariante.
Derivación de bucles.

Tripleta de Hoare: {Q} S {R}

Como se observa en la gráfica el

invariante { I } describe el estado de la
construcción:
 Antes del bucle, I
 Durante sus iteraciones {I ʌ B}
 A su salida {I ʌ ¬B}

Con respecto al bucle es de anotar lo siguiente:

{ Q } S0 { I } El invariante se satisface antes de la primera iteración.

{IʌB} S {I} El invariante se mantiene al ejecutar el cuerpo S del bucle.
{IʌB}C≥0 La función cota es ≥ 0 cuando se cumple la condición B
{I ʌ B ʌ C=T} S {C < T} La función de cota decrece al ejecutarse el cuerpo del bucle.
{ I ʌ ¬B }  { R } El invariante se cumple al salir del bucle

Luego,

En el caso de derivación del código de un bucle debe determinarse:

 El invariante, I
  Las condiciones B y ¬B
 Las instrucciones S0 de asignación de variables.
 Las instrucciones S del cuerpo del bucle, las cuales están constituidas por dos
instrucciones fundamentales:
S1, instrucción(es) que se encarga(n) de mantener cierto el invariante
S2, instrucción que hace que las variables que intervienen en B avancen hacia el
estado de terminación del bucle.
 La función cota, C.

En este contexto, para derivar un bucle se sigue el siguiente esquema:

{Q}
S0;
{ I, C }
Mientras (B)
S1;
S2;
Fin-Mientras
{R}

Específicamente, la derivación de un bucle se hace a través de los siguientes pasos:

B.1 Obtención del invariante.

 Las condiciones que se incluyan en el invariante deben ser fáciles de conseguir a

partir de la postcondición.
 El invariante ha de ser lo bastante débil para que se pueda obtener de la
precondición.
 El invariante ha de ser lo bastante fuerte para que junto con la condición de
terminación implique a la postcondición.
 Se recomienda reforzar el invariante con condiciones que aparezcan en la
precondición.

Existen dos posibilidades en la definición del invariante:

 Si la postcondición está en forma conjuntiva, se pueden ensayar distintas

posibilidades eligiendo una parte ella como invariante y el resto como negación de la
condición del bucle.
  Se puede introducir una nueva variable que sustituya en la postcondición a una
constante. En este caso el invariante será la postcondición generalizada con esa
nueva variable y la condición del bucle será la negación de la igualdad entre la
variable y la constante sustituida.

B.2 Obtención de condición de repetición.

La condición de repetición es B
La condición de terminación es ¬B

Se debe probar que { I ʌ ¬B }  { R }

B.3 Definición de la condición de repetición.

Se debe probar que I  def(B) (Que I permita definir a B)

Luego, I garantiza que la condición de repetición se puede evaluar.

En ocasiones no será así porque en B (y en I) pueden aparecer variables nuevas (al

sustituir constantes por variables). En ese caso se deberán introducir con una
declaración local.

B.4 Expresión de acotación.

La cota debe definirse teniendo en cuenta las variables que intervienen en el control del
bucle, de tal manera que asegure su decrecimiento con cada ejecución.

Considerando I, B se construye una expresión de acotación C.

Se debe probar que { I ʌ B }  def(C) ʌ dec(C)

Para obtener expresiones de acotación, se recomienda observar la condición de

terminación, así como las variables que se modifican en el bucle.

Luego, se debe cumplir que { I ʌ B }  C ≥ 0

B.5 Acción de inicialización de variables, S0.

Diseñar S0 (instrucciones de inicialización) para las variables que aparecen en el invariante
de modo que el este sea verdadero, es decir
 Diseñar S0 tal que { Q } S0 { I }

Nota. Si la precondición no garantiza que se cumple el invariante antes de entrar en el bucle, entonces
es necesario derivar una acción de inicialización que establezca el invariante. Esta acción se deriva a
partir de la especificación {Q } S0 { I }

B.6 Acción de avance.

Se deriva una acción S2 que haga avanzar al bucle hacia su terminación. Esta instrucción es
fácil de deducir puesto que se conoce el valor inicial de las variables dado por S0 y la
condición ¬B que hace terminar al bucle.

Se puede derivar a partir de la especificación

Derivar S2 a partir de { I ʌ B ʌ C = T } S2 { C < T }

Nota. El cuerpo del ciclo consistirá de una instrucción avanzar S 2 que permita avanzar hacia ¬B para
garantizar la finalización del bucle y la instrucción restablecer S 1 de tal manera que asegure el
cumplimiento del invariante dentro del bucle.

B.7 Evaluación de la acción de avance.

Hay que confirmar si la acción de avance constituye el cuerpo del bucle. Para ello, se debe
demostrar

Demostrar que { B ʌ I } S2 { I }

Si se cumple, entonces hemos acabado de obtener un algoritmo correcto.

B.8 Restablecimiento del invariante.

Si la acción de avance no es suficiente (lo más habitual), entonces se necesita derivar una
nueva acción S1 que se encargue de restablecer el invariante dentro del bucle, de forma que

{ I ʌ B } S1 ; S2 { I }

Derivar S1 de la especificación { I ʌ B } S1 { R } donde R = pmd( S2, I )

B.9 Terminación.
Se comprueba que después de introducir la acción S1 se sigue cumpliendo

{ I ʌ B ʌ C = T } S1 ; S2 { C < T }
 Si se comprueba, entonces hemos acabado de obtener un algoritmo correcto.
Para comprobar lo anterior, se debe obtener la pmd de { C < T } y verificar que
{ I ʌ B ʌ C = T } es más fuerte que ella.

El esquema general resultante de la derivación de un bucle es de la forma:

var x1:t1; …;xn:tn;

{Q}
inicialización
inicio
S0;
{I}
it B
{IʌB}
S1;
{T}
S2;
{I}
Fin-it
{ I ʌ ¬B }
fin
{R}

Ejemplo_1: Sea la siguiente especificación:

{ Q: x=X ʌ y = Y ʌ x ≥ 0 ʌ y > 0 }
divMod
{ R: x = X ʌ y = Y ʌ x = c*y + r ʌ 0≤ r ʌ r < y }

Derivar el código correspondiente.

Análisis:

x y
ej. 7 | 2
1 3
r c

Podemos obtener el cociente como el número de veces que hay que restarle y a x
para obtener un valor menor que y, siendo este el resto.

luego, 7- 2-2-2 =1 x - y… - y = r
 c veces

Luego, determinamos que el algoritmo va a ser un bucle. Entonces derivar un bucle.

B.1 Obtención del invariante. Se efectúa a partir de la postcondición.

 Los predicados relativos a la conservación de valores x = X ʌ y = Y

pasan a ser parte del invariante.

 La condición de terminación es que r < y. Luego, restaremos hasta que r < y.

Prueba de escritorio
x y r c r<y ? x = c*y + r
7 2 5 1 5<2 F
7 = 1*2 + 5
3 2 3<2 F
7 = 2*2 + 3
1 3 1<2 V 7 = 3*2 + 1

acción de avance del bucle

x y
ej. 7 | 2
1 3
r c

luego, 7- 2-2-2 =1 x - y… - y = r
c veces

Condición de terminación: r < y

Luego en invariante es : { I : x = X ʌ y = Y ʌ x = c*y + r ʌ r ≥ 0 ʌ y > 0 }
La postcondición dada es : { R : x = X ʌ y = Y ʌ x = c*y + r ʌ r ≥ 0 ʌ r < y }

El invariante se considera como la postcondición generalizada.

B.2 Obtención de condición de repetición.

Con el invariante y la postcondición obtenemos la condición de terminación.

La condición de terminación es: ¬B: r < y

Se debe probar que se cumpla: { I ʌ ¬B }  { R }

{ I ʌ ¬B } : x = X ʌ y = Y ʌ x = c*y + r ʌ r ≥ 0 ʌ y > 0 ʌ r < y

r≥0ʌy>0 ʌr<y: 0≤r<y

 { I ʌ ¬B } : x = X ʌ y = Y ʌ x = c*y + r ʌ 0 ≤ r < y = { R }

{ R: x = X ʌ y = Y ʌ x = c*y + r ʌ 0 ≤ r ʌ r < y }

Luego, la condición de terminación se cumple.

B.3 Definición de la condición de repetición.

Se debe probar si I  def(B) (Que I permita definir a B)

I garantiza que la condición de repetición se puede evaluar.

Condición de repetición según la prueba de escritorio B: r ≥ y

{ I : x = X ʌ y = Y ʌ x = c*y + r ʌ r ≥ 0 ʌ y > 0 }

r ≥ 0 ʌ y > 0 : r ≥ y : verdadero.

B.4 Expresión de acotación.

Considerando I, B se construye una expresión de acotación C.

Se debe probar que { I ʌ B }  def(C) ʌ dec(C)

Para obtener expresiones de acotación, se recomienda observar la condición de terminación, así como
las variables que se modifican en el bucle.

{ I ʌ B }  def(C) ʌ dec(C)

Nota. La cota debe definirse teniendo en cuenta las variables que intervienen en el control del bucle,
de tal manera que se asegure su decrecimiento con cada ejecución.
Luego, { I ʌ B}  C≥0

{ I : x = X ʌ y = Y ʌ x = c*y + r ʌ r ≥ 0 ʌ y > 0 }

{ I ʌ B }: x = X ʌ y = Y ʌ x = c*y + r ʌ r ≥ 0 ʌ y > 0 ʌ r ≥ y

Se observa en B que (r ≥ y) y considerando que r va decreciendo en cada pasada por

el bucle, se toma a r como expresión de acotación.

Luego, def(C) = def(r) = cierto.

Variable que decrece: r. Luego, C(r) = r ≥ 0

B.5 Acción de inicialización.

Se inicializan las variables de modo que el invariante sea cierto.

Diseñar S0 de modo que el invariante sea verdadero, es decir que

Diseñar S0 tal que { Q } S0 { I }

{ Q: x=X ʌ y = Y ʌ x ≥ 0 ʌ y > 0 } S0 { I : x = X ʌ y = Y ʌ x = c*y + r ʌ r ≥ 0 ʌ y > 0 }

Como se observa la fórmula que describe el comportamiento del invariante es

x = c*y + r

Luego, se toma como acción de inicialización, considerando que r decrece a partir

del valor de x y es la cota, y que la variable c se incrementa a partir de 1.

Luego, < c, r > = < 0, x >

Reescribiendo la tripleta de Hoare:

{ Q: x=X ʌ y = Y ʌ x ≥ 0 ʌ y > 0 }

c = 0; r = x;
{ I : x = X ʌ y = Y ʌ x = c*y + r ʌ r ≥ 0 ʌ y > 0 }

Verificación:
{ Q: x=X ʌ y = Y ʌ x ≥ 0 ʌ y > 0 } c = 0; { M }
{M} r = x; { I : x=X ʌ y=Y ʌ x=c*y+r ʌ r ≥ 0 ʌ y >0 }

Para {M} M=IEx = ( x = X ʌ y = Y ʌ x = c*y + r ʌ r ≥ 0 ʌ y > 0 )|xr

Igualando : ( x = X ʌ y = Y ʌ x = c*y + x ʌ x ≥ 0 ʌ y > 0 )
Luego { M : ( x = X ʌ y = Y ʌ c*y = 0 ʌ x ≥ 0 ʌ y > 0 ) }

Para {Q} Q=MEx = ( x = X ʌ y = Y ʌ c*y = 0 ʌ x ≥ 0 ʌ y > 0 )|0c

Igualando : ( x = X ʌ y = Y ʌ 0*y = 0 ʌ x ≥ 0 ʌ y > 0 )
: (x=Xʌy=Yʌx≥0ʌy>0)

Luego, se cumple que {Q} S0 {I}

B.6 Acción de avance.

Se deriva una acción (instrucción) S2 que haga avanzar al bucle hacia ¬B (condición de
terminación).
  Se sabe que si x=r < y entonces en bucle no ejecuta ninguna vez.
 Si x > y entonces se entra al bucle que debe decrementar el valor de r.

Luego, la instrucción (acción) de avance del bucle es: r = r - y

Luego, se debe probar que se cumple { I ʌ B ʌ C = T } S2 { C < T } para comprobar

que el bucle termina.

Para probar que esta tripla es correcta se debe demostrar que

{ I ʌ B ʌ C=T }  pmd( S2, C < T) : pmd( r = r - y, r < T )

pmd( r = r - y, r < T ) = (r < T)| r-yr = ( r - y ) < T

Luego, se debe probar que { I ʌ B ʌ C=T }  ( r - y ) < T

Si r = T  ( r - y ) < T Lo cual es verdadero.

B.7 Evaluación de la acción de avance.

Se debe probar si la acción de avance constituye el cuerpo del bucle. Para ello, se debe
demostrar:

{ B ʌ I } S2 { I } Si se cumple, entonces hemos acabado de obtener el

algoritmo correcto de un bucle.

Luego, { M: r ≥ y ʌ x = X ʌ y = Y ʌ x = c*y + r ʌ r ≥ 0 ʌ y > 0 }

r = r - y;
{ I: x = X ʌ y = Y ʌ x = c*y + r ʌ r ≥ 0 ʌ y > 0 }

Verificación.

Para {M} M=IEx = (x = X ʌ y = Y ʌ x = c*y + r ʌ r ≥ 0 ʌ y > 0)|r-yr

Igualando : x = X ʌ y = Y ʌ x = c*y + (r-y) ʌ (r-y) ≥ 0 ʌ y > 0
Resolviendo : x = X ʌ y = Y ʌ x = c*y + r - y ʌ r ≥ y ʌ y > 0
: x = X ʌ y = Y ʌ x = c*y + r - y ʌ r ≥ y ʌ y > 0
{M : x = X ʌ y = Y ʌ x = (c-1)*y + r ʌ r ≥ y ʌ y > 0 } : pmd
Luego, no se cumple porque (x = c*y + r) <> (x = (c-1)*y + r )
B.8 Restablecimiento del invariante.
Si la acción de avance no es suficiente, entonces necesitamos derivar una nueva acción S1
que se encargue de restablecer el invariante dentro del bucle, de forma que

{ I ʌ B } S1 ; S2 { I }
donde S1 se puede derivar de la especificación
{ I ʌ B } S1 { R } donde R = pmd( S2, I )

Luego: { I ʌ B : x = X ʌ y = Y ʌ x = c*y + r ʌ r ≥ 0 ʌ y > 0 ʌ r ≥ y }

S1
{ R: x = X ʌ y = Y ʌ x = (c-1)*y + r ʌ r ≥ y ʌ y > 0 }

Para que { x = c*y + r } S1 { x = (c-1)*y + r }

Entonces S1: c = c + 1

Verificación. pmd(c=c+1, x = (c-1)*y + r)

= (x = (c-1)*y + r)c+1c : x = ((c+1)-1)*y + r = c*y + r

B.9 Terminación.
Se comprueba que después de introducir la acción S1 no se afecta la terminación del bucle,
es decir que se sigue cumpliendo

{ I ʌ B ʌ C = T } S1 ; S2 { C < T }

Si se comprueba, entonces hemos acabado de obtener un algoritmo

correcto.

Verificar { I ʌ B ʌ r = T } c=c+1; r=r-y { T }

{ M: I ʌ B ʌ r = T } c=c+1; { N }
{ N } r=r-y {U: r < T }

{N} r=r-y
N = UEx = ( r < T )Ex = (r - y) < T

{M} c=c+1
M=NEx = ((r-y) < T)| Ex = ((r-y) < T) : pmd
 Luego, se debe probar que { I ʌ B ʌ C=T }  ( r - y ) < T
Si r = T  ( r - y ) < T Lo cual es verdadero.

Luego la especificación del código derivado es:

var x, y, c, r : entero
{ Q: x = X ʌ y = Y ʌ x ≥ 0 ʌ y > 0 }
inicio
c=0;
r=x;
{ I : x = X ʌ y = Y ʌ x = c*y + r ʌ r ≥ 0 ʌ y > 0 }
it r ≥ y
{I ʌ B} = { x = X ʌ y = Y ʌ x = c*y + r ʌ r ≥ 0 ʌ y > 0 ʌ r ≥ y }
c=c+1;
{ M: x=X ʌ y = Y ʌ x = (c-1)*y + r ʌ r ≥ y ʌ y > 0 }
r=r-y;
{ I : x = X ʌ y = Y ʌ x = c*y + r ʌ r ≥ 0 ʌ y > 0 }
fin-it
{ I ʌ ¬B } = { x = X ʌ y = Y ʌ x = c*y + r ʌ r ≥ 0 ʌ y > 0 ʌ r<y }
{ R: x = X ʌ y = Y ʌ x = c*y + r ʌ 0 ≤ r ʌ r < y }

El seudocódigo derivado es:

Prueba de escritorio
entero x, y, c, r;
c=0; x y c r r≥y ?
7 2 0 7 7≥2 V
r=x;
1 5 5≥2 V
Mientras(r ≥ y)
2 3 3≥2 V
c=c+1;
3 1 1≥2 F
r=r-y;
Fin-Mientras
x = c*y + r
7 = 0*2 + 7
7 = 1*2 + 5
7 = 2*2 + 3
7 = 3*2 + 1

---------------- Fin de documento