1poscondicion conjuntiva

Caso 2: La postcondición está en forma conjuntiva.
Se elige una parte como invariante y el resto como negación de la condición del bucle
Ejemplo : Búsqueda Secuencial

Derivar un algoritmo que paraun arreglo V[0..N) de números enteros, permita
obtener el menor índice donde se encuentra una constante entera k. Si ninguna
componente es k, el algoritmo devuelve N.
entero x
constante entero k
{P:N≥0}
Mientras (B)
:
FinMientras

{Q : ( 0≤x≤N) ^<∀j: 0≤ j
x es el primer valor entre 0 y N que cumple que todas las componentes anteriores no
son la constante K

1.Diseñar el invariante I y la condición del bucle a partir de la
postcondición, sabiendo que se debe cumplir que I ^~B=> Q.

{Q: ( 0≤x≤N ^<∀ j: 0≤ j)

^ ((V[x]=k) v (x=N))

I: (0≤x≤N) ^ < ∀ j: 0≤j
~ B: ( V[x]=k) v (x=N )  B:( V[x] ≠k) ^ (x≠N )
B: (x≠N ) ^ ( V[x] ≠k)

2.Diseñar A0 de modo que el invariante sea cierto {P} A0 {I}

{P}  pmd(A0 , I)

I: (0≤x≤N) ^ < ∀ j: 0≤ j

x es la única variable de programa que aparece en la condición y en el invariante, debe ser
inicializada.

pmd(A0,I) ≡ pmd(x=E ,I ) ≡ ( 0≤x≤N ^ (∀ j:0≤ j ≡ ( 0≤ E≤N ) ^ (<∀ j: 0≤j).
(1)

(2)

Como se debe inicializar x, se toma el valor más pequeño de E, por (1) se elige E=0,

En (2) por ser el rango vacío, la segunda expresión de la conjunción es TRUE
pmd(A0,I)≡(0≤ N) ^ TRUE ≡ 0≤ N ≡ {P }

Como {P}  pmd(A0, I), es válida la inicialización x =0

3. Diseñar el cuerpo del ciclo.
Esto implica diseñar la instrucción A2 para avanzar de modo que decrezca lafunción cota.
Como x se inicializa en 0, debe crecer dentro del bucle.
Elegimos entonces como instrucción A2 de avance a x=x + 1
Se debe probar que {I ^ B} A2 {I} es correcto
{I ^ B}  pmd( A2, I)
I:(0≤x≤N) ^ < ∀ j: 0≤ j

B: (x≠N ) ^ ( V[x] ≠k)

pmd(A2 ,I) ≡ pmd(x=x+1 ,I) ≡ (I)x x+1 ≡ (0≤x+1≤N) ^ <∀ j:0≤ j
partición de rango

≡ (0≤x+1 ≤N) ^ <∀ j:0≤ j ^ v[x]≠k...

Leer documento completo

Regístrate para leer el documento completo.