guia03.txt

Tomando def(x) = True para toda x variable o constante,

1.a.
def(a + 1) ≡ True
1.b.
def(a/b) ≡ (b != 0)
1.c.
def(sqrt(a/b)) ≡ ((b != 0) ^L (a/b >= 0))
1.d.
def(A[i] + 1) ≡ (0 <= i < |A|)
1.e.
def(A[i+2]) ≡ (0 <= i+2 < |A|)
1.f.
def((0 <= i <= |A|) ^L (A[i] >= 0)) ≡ (i != |A|)

2.a.
{wp(a := a+1, Q2)} ≡ {def(a + 1) ^L a + 1 >= 0} ≡ {Q3} ≡ {a >= -1}
a := a+1
{wp(b := a/2, Q1)} ≡ {def(a/2) ^L a/2 >= 0} ≡ {True ^L a/2 >= 0} ≡ {Q2} ≡ {a >= 0} 
b := a/2
{Q1} ≡ {b >= 0}
2.b.
wp(a := A[i] + 1, Q2) ≡ {Q3} ≡ {(0 <= i < |A|) ^L ((A[i] != sqrt(2)) - 1 ^ (A[i] != -sqrt(2) - 1))} 
a := A[i] + 1
wp(b := a*a, Q1) ≡ {Q2} ≡ {a*a != 2} ≡ {|a| != sqrt(2)} ≡ {a != sqrt(2) ^ a != -sqrt(2)}
b := a*a
{Q1} ≡ {b != 2}
2.c.
wp(a := A[i] + 1, Q2) ≡ {Q3} ≡ {(0 <= i < |A|) ^L (b != 0)}
a := A[i] + 1
wp(a := b*b, Q1) ≡ {b*b >= 0} ≡ {Q2} ≡ {b != 0}
a := b*b
{Q1} ≡ {a >= 0}
2.d.
wp(a := a - b, Q2) ≡ {(a - b >= 0) ^ (a - b + b >= 0)} ≡ {Q3} ≡ {(a >= 0) ^ (a >= b)}
a := a - b
wp(b := a + b, Q1) ≡ {Q2} ≡ {(a >= 0) ^ (a + b >= 0)}
b := a + b
{Q1} ≡ {a >= 0 ^ b >= 0}

3.a.
wp(A[i] := 0, Q) ≡ wp(A := setAt(A,i,0), Q) ≡
{(0 <= i < |A|) ^L (∀j: Z)((0 < j < |setAt(A,i,0)|) =>L (setAt(A,i,0)[j] >= 0))} ≡
{(0 <= i < |A|) ^L (∀j: Z)(((0 < j < |A|) ^ (j != i)) =>L (A[j] >= 0))}

3.b.
wp(A[i+2] := 0, Q) ≡ wp(A := setAt(A,i+2,0), Q) ≡
{(-2 <= i < |A|-2) ^L (∀j: Z)((0 < j < |setAt(A,i+2,0)|) =>L (setAt(A,i+2,0)[j] >= 0))} ≡
{(-2 <= i < |A|-2) ^L (∀j: Z)(((0 < j < |A|) ^ (j != i+2)) =>L (A[j] >= 0))}

3.c.
wp(A[i+2] := -1, Q) ≡ wp(A := setAt(A,i+2,-1), Q) ≡ {False}

3.d.
wp(A[i] := 2*A[i], Q) ≡ wp(A := setAt(A,i,2*A[i]), Q) ≡
{(0 <= i < |A|) ^L (∀j: Z)((0 < j < |setAt(A,i,2*A[i])|) =>L (setAt(A,i,2*A[i])[j] >= 0))} ≡
{(0 <= i < |A|) ^L (∀j: Z)((0 < j < |A|) =>L (A[j] >= 0))}

3.e.
wp(A[i] := A[i-1], Q) ≡ wp(A := setAt(A,i,A[i-1]), Q) ≡
{(1 <= i < |A|) ^L (∀j: Z)((0 < j < |setAt(A,i,A[i-1])|) =>L (setAt(A,i,A[i-1])[j] >= 0))} ≡
{(1 <= i < |A|) ^L (∀j: Z)(((0 < j < |A|) ^ (j != i)) =>L (A[j] >= 0))}

4.a.
wp(b := a, Q) ≡ {a = -|a|} ≡ {a <= 0}
wp(b := -a, Q) ≡ {-a = -|a|} ≡ {a >= 0}
wp(S, Q) ≡ {def(a < 0) ^L (((a < 0) ^ wp(b := a, Q)) v ((a >= 0) ^ wp(b := -a, Q)))} ≡
{((a < 0) ^ wp(b := a, Q)) v ((a >= 0) ^ wp(b := -a, Q))} ≡
{((a < 0) ^ (a <= 0)) v ((a >= 0) ^ (a >= 0))} ≡
{(a < 0) v (a >= 0)} ≡
{True}

4.b.
wp(b := a, Q) ≡ {a = |a|} ≡ {a >= 0}
wp(b := -a, Q) ≡ {-a = |a|} ≡ {a <= 0}
wp(S, Q) ≡ {def(a < 0) ^L (((a < 0) ^ wp(b := a, Q)) v ((a >= 0) ^ wp(b := -a, Q)))} ≡
{((a < 0) ^ (a >= 0)) v ((a >= 0) ^ (a <= 0))} ≡
{False v (a = 0)} ≡
{a = 0}

4.c.
wp(s[i] := 0, Q) ≡ wp(s := setAt(s,i,0), Q) ≡
{(0 <= i < |s|) ^L (∀j: Z)((0 <= j < |setAt(s,i,0)|) =>L (setAt(s,i,0)[j] >= 0))} ≡
{(0 <= i < |s|) ^L (∀j: Z)(((0 <= j < |s|) ^ (j != i)) =>L (s[j] >= 0))}
wp(s[0] := 0, Q) ≡ wp(s := setAt(s,0,0), Q) ≡
{(0 < |s|) ^L (∀j: Z)((0 <= j < |setAt(s,0,0)|) =>L (setAt(s,0,0)[j] >= 0))} ≡
{(0 < |s|) ^L (∀j: Z)((1 <= j < |s|) =>L (s[j] >= 0))} ≡
{(∀j: Z)((1 <= j < |s|) =>L (s[j] >= 0))}
wp(S, Q) ≡ {def(i > 0) ^L (((i > 0) ^ ((0 <= i < |s|) ^L (∀j: Z)(((0 <= j < |A|) ^ (j != i)) =>L (s[j] >= 0)))) v ((i <= 0) ^ (∀j: Z)((1 <= j < |s|) =>L (s[j] >= 0))))} ≡
{((1 <= i < |s|) ^L (∀j: Z)(((0 <= j < |s|) ^ (j != i)) =>L (s[j] >= 0))) v ((i <= 0) ^ (∀j: Z)((1 <= j < |s|) =>L (s[j] >= 0)))} ≡ /* todos salvo s[i] tienen que ser >= 0 v todos salvo s[0 = i] tienen que ser >= 0 */
{(0 <= i < |s|) ^L (∀j: Z)(((0 <= j < |s|) ^ (j != i)) =>L (s[j] >= 0))}

4.d.
wp(s[i] := s[i-1], Q) ≡ wp(s := setAt(s,i,s[i-1]), Q) ≡
{(1 <= i < |s|) ^L (∀j: Z)((0 <= j < |setAt(s,i,s[i-1]|) =>L (setAt(s,i,s[i-1])[j] = setAt(s,i,s[i-1])[j-1]))} ≡
{(1 <= i < |s|) ^L (∀j: Z)(((0 <= j < |s|) ^ (j != i)) =>L (s[j] = s[i-1]))}
wp(s[i] := 0, Q) ≡ wp(s := setAt(s,i,0), Q) ≡
{(0 <= i < |s|) ^L (∀j: Z)((0 <= j < |setAt(s,i,0)|) =>L (setAt(s,i,0)[j] = setAt(s,i,0)[j-1]))} ≡
{(0 <= i < |s|) ^L (∀j: Z)(((0 <= j < |s|) ^ (j != i)) =>L (s[j] = 0))}
wp(S, Q) ≡ {def(i > 1) ^L (((i > 1) ^ ((1 <= i < |s|) ^L (∀j: Z)(((0 <= j < |s|) ^ (j != i)) =>L (s[j] = s[i-1])))) v ((i <= 1) ^ ((0 <= i < |s|) ^L (∀j: Z)(((0 <= j < |s|) ^ (j != i)) =>L (s[j] = 0)))))} ≡
{((2 <= i < |s|) ^L (∀j: Z)(((0 <= j < |s|) ^ (j != i)) =>L (s[j] = s[i-1]))) v ((0 <= i < 2) ^L (∀j: Z)(((0 <= j < |s|) ^ (j != i)) =>L (s[j] = 0)))}

4.e.
wp(s[i] := -s[i], Q) ≡ wp(s := setAt(s,i,-s[i]), Q) ≡
{(0 <= i < |s|) ^L (0 <= i < |setAt(s,i,-s[i]|) ^L (setAt(s,i,-s[i])[i] >= 0)} ≡
{(0 <= i < |s|) ^L (0 <= i < |s|) ^L (s[i] <= 0)} ≡
{(0 <= i < |s|) ^L (s[i] <= 0)}
wp(skip, Q) ≡ {Q}
wp(S, Q) ≡ {def(s[i] < 0) ^L (((s[i] < 0) ^ ((0 <= i < |s|) ^L (s[i] <= 0))) v ((s[i] >= 0) ^ ((0 <= i < |s|) ^L (s[i] >= 0))))} ≡
{(0 <= i < |s|) ^L (((s[i] < 0) ^ ((0 <= i < |s|) ^L (s[i] <= 0))) v ((s[i] >= 0) ^ ((0 <= i < |s|) ^L (s[i] >= 0))))} ≡
{(0 <= i < |s|) ^L (((s[i] < 0) ^ (s[i] <= 0)) v ((s[i] >= 0) ^ (s[i] >= 0)))} ≡
{(0 <= i < |s|) ^L ((s[i] < 0) v (s[i] >= 0))} ≡
{(0 <= i < |s|) ^L True)} ≡
{0 <= i < |s|}

4.f.
wp(s[i] := -s[i], Q) ≡ wp(s := setAt(s,i,-s[i]), Q) ≡
{(0 <= i < |s|) ^L (∀j: Z)((0 <= j < |setAt(s,i,-s[i])|) =>L (setAt(s,i,-s[i])[j] >= 0))} ≡
{(0 <= i < |s|) ^L (∀j: Z)((0 <= j < |s|) =>L (setAt(s,i,-s[i])[j] >= 0))} ≡
{(0 <= i < |s|) ^L (∀j: Z)(((0 <= j < |s|) ^ (j != i)) =>L (s[j] >= 0)) ^ (s[i] <= 0)}
wp(skip, Q) ≡ {Q}
wp(S, Q) ≡ {def(s[i] > 0) ^L (((s[i] > 0) ^ ((0 <= i < |s|) ^L (∀j: Z)(((0 <= j < |s|) ^ (j != i)) =>L (s[j] >= 0)) ^ (s[i] <= 0))) v ((s[i] <= 0) ^ ((∀j: Z)((0 <= j < |s|) =>L (s[j] >= 0)))))} ≡
{(0 <= i < |s|) ^L (((s[i] > 0) ^ (∀j: Z)(((0 <= j < |s|) ^ (j != i)) =>L (s[j] >= 0)) ^ (s[i] <= 0)) v ((s[i] <= 0) ^ (∀j: Z)((0 <= j < |s|) =>L (s[j] >= 0))))} ≡
{(0 <= i < |s|) ^L (False v ((s[i] <= 0) ^ (∀j: Z)((0 <= j < |s|) =>L (s[j] >= 0))))} ≡
{(0 <= i < |s|) ^L ((s[i] = 0) ^ (∀j: Z)(((0 <= j < |s|) ^ (j != i)) =>L (s[j] >= 0)))}

5.a.
int sumarElemento(int[] s, int i, int a) {
    a += s[i]; /* a := a + s[i] */ 
    return a;
}
S ≡ a := a + s[i]
wp(S, asegura) ≡ {(0 <= i < |s|) ^L (a + s[i] = Σ(j=0;i)(s[j]))} ≡
{(0 <= i < |s|) ^L (a = Σ(j=0;i)(s[j]) - s[i])} ≡
{(0 <= i < |s|) ^L (a = Σ(j=0;i-1)(s[j]))} 
requiere => wp(S, asegura) ≡ requiere => requiere ≡ True
El programa es correcto, pues wp(S, asegura) es exactamente el requiere del enunciado.

5.b.
int restarPrimero(int[] s, int a) { /* int i innecesario */
    a -= s[0]; /* a := a - s[0] */ 
    return a;
}
S ≡ a := a - s[0]
wp(S, asegura) ≡ {(0 < |s|) ^L (a - s[0] = Σ(j=1;i)(s[j]))} ≡
{(0 < |s|) ^L (a = Σ(j=1;i)(s[j]) + s[0])} ≡
{(0 < |s|) ^L (a = Σ(j=0;i)(s[j]))}
requiere => wp(S, asegura) ≡ ((0 <= i < |s|) ^L (a = Σ(j=0;i)(s[j]))) => ((0 < |s|) ^L (a = Σ(j=0;i)(s[j]))) ≡ True
El programa es correcto, pues el requiere del enunciado implica a la wp(S, asegura) encontrada.

5.c.
boolean elementoNoNegativo(int[] s, int i) {
    res = s[i] >= 0; /* res := s[i] >= 0 */
    return res; 
}
S ≡ res := s[i] >= 0
wp(S, asegura) ≡ {(0 <= i < |s|) ^L ((s[i] >= 0) <=> (∀j: Z)((0 <= j <= i) =>L (s[j] >= 0)))} ≡
{(0 <= i < |s|) ^L (∀j: Z)((0 <= j < i) =>L (s[j] >= 0))}
requiere => wp(S, asegura) ≡ requiere => requiere ≡ True
El programa es correcto, pues wp(S, asegura) es exactamente el requiere del enunciado.

5.d.
int incrementarSiElementoNoNulo(int[] s, int i, int a) {
    if (s[i] != 0) {
        a += 1; /* a := a + 1 */
    } /* else {skip} */
    return a;
}
S ≡
if (s[i] != 0)
    a := a + 1
else
    skip
endif
wp(S, asegura) ≡ {def(s[i] != 0) ^L (((s[i] != 0) ^ (a + 1 = Σ(j=0;i)(Beta(s[j] != 0)))) v ((s[i] = 0) ^ (asegura)))} ≡
{(0 <= i < |s|) ^L (((s[i] != 0) ^ (a = Σ(j=0;i)(Beta(s[j] != 0)) - 1)) v ((s[i] = 0) ^ (a = Σ(j=0;i)(Beta(s[j] != 0)))))} ≡
{(0 <= i < |s|) ^L (((s[i] != 0) ^ (a = Σ(j=0;i-1)(Beta(s[j] != 0)))) v ((s[i] = 0) ^ (a = Σ(j=0;i-1)(Beta(s[j] != 0)))))} ≡
{(0 <= i < |s|) ^L (a = Σ(j=0;i-1)(Beta(s[j] != 0)))}
requiere => wp(S, asegura) ≡ requiere => requiere ≡ True
El programa es correcto, pues wp(S, asegura) es exactamente el requiere del enunciado.

5.e.
int incrementarSiPrimeroNoNulo(int[] s, int a) { /* int i innecesario */
    if (s[0] != 0) {
        a += 1; /* a := a + 1 */
    } /* else {skip} */
    return a;
}
S ≡
if (s[0] != 0)
    a := a + 1
else
    skip
endif
wp(S, asegura) ≡ {def(s[0] != 0) ^L (0 <= i < |s|) ^L (((s[0] != 0) ^ (a + 1 = Σ(j=0;i-1)(Beta(s[j] != 0)))) v ((s[0] = 0) ^ (asegura)))} ≡
{(0 < |s|) ^L (((s[0] != 0) ^ (a + 1 = Σ(j=0;i-1)(Beta(s[j] != 0)))) v ((s[0] = 0) ^ (a = Σ(j=0;i-1)(Beta(s[j] != 0)))))} ≡
{(0 < |s|) ^L (((s[0] != 0) ^ (a = Σ(j=0;i-1)(Beta(s[j] != 0)) - 1)) v ((s[0] = 0) ^ (a = Σ(j=0;i-1)(Beta(s[j] != 0)))))} ≡
{(0 < |s|) ^L (((s[0] != 0) ^ (a = Σ(j=1;i-1)(Beta(s[j] != 0)))) v ((s[0] = 0) ^ (a = Σ(j=1;i-1)(Beta(s[j] != 0)))))} ≡
{(0 < |s|) ^L (a = Σ(j=1;i-1)(Beta(s[j] != 0)))}
requiere => wp(S, asegura) ≡ ((0 <= i < |s|) ^L (a = Σ(j=1;i-1)(Beta(s[j] != 0)))) => ((0 < |s|) ^L (a = Σ(j=1;i-1)(Beta(s[j] != 0)))) ≡ True
El programa es correcto, pues el requiere del enunciado implica a la wp(S, asegura) encontrada.

###
Teorema de corrección de un ciclo
El teorema dice que un ciclo termina y es correcto respecto de su especificación si:
1. P_c => I (I vale antes del ciclo)
2. {I ^ B} S {I} (el invariante sigue valiendo después de cada iteración del ciclo, y la wp del programa dentro del ciclo implica (I ^ B), lo que a su vez implica que I debe valer al comienzo de cada iteración)
3. (I ^ ¬B) => Q_c (I vale después del ciclo)
4. {I ^ B ^ v0 = fv} S {fv < v0} (la función variante disminuye en valor en cada iteración del ciclo)
5. (I ^ fv <= 0) => ¬B (el ciclo termina cuando la función variante se hace no positiva)
Donde B es la condición del ciclo, S el programa ejecutado dentro del ciclo, y P_c, Q_c son la pre y postcondición del ciclo, respectivamente.
Obs.: El teorema requiere de la aplicación del teorema del invariante (1-3) y el teorema de terminación de ciclo (4-5). El teorema de terminación nos asegura que el ciclo termina, condición necesaria para que valga el teorema del invariante, que asegura la correctitud del ciclo, es decir la validez de la tripla de Hoare {P_c} while B do S endwhile {Q_c}.
Obs.: No hay método mecánico para derivar el invariante, I, ni la función variante, fv. Si el ciclo es parte intermedia de un programa más grande (como casi siempre lo és) tampoco hay método mecánico para definir cuál es su precondición y postcondición, P_c y Q_c.
Obs.: No nos permite encontrar la wp del ciclo, sólo demostrar que la P_c propuesta o dada implica la wp del ciclo (demostrando por lo tanto la validez de la tripla).
###

6.a.
P_c ≡ {res = 0 ^ i = 0}
Q_c ≡ {res = Σ(j=0;|s|-1)(s[j])}
6.b.
- El invariante no valdría después del ciclo (fallaría el punto 3)
- El invariante no valdría después de la última iteración del ciclo (fallaría el punto 2)
6.c.
Ese cambio haría que el invariante pueda indefinirse.
- El invariante no valdría después del ciclo (fallaría el punto 3)
- El invariante no valdría después de la última iteración del ciclo (fallaría el punto 2)
6.d.
- El invariante no valdría después del ciclo (fallaría el punto 3)
- El invariante no valdría después de cada iteración del ciclo (fallaría el punto 2)

6.e.
1. QVQ P_c => I ≡ {(res = 0 ^ i = 0) => (0 <= i <= |s| ^L res = Σ(j=0;i-1)(s[j]))} ≡ True /* Cuando los extremos no son válidos la sumatoria da 0, la productoria 1 */
2. QVQ (I ^ B) => wp(S, I)
Con S ≡
res := res + s[i];
i := i + 1;
wp(i := i + 1, I) ≡ {0 <= i+1 <= |s| ^L res = Σ(j=0;i)(s[j])} ≡ {Q}
wp(res := res + s[i], Q) ≡ {(0 <= i < |s|) ^L (0 <= i+1 <= |s| ^L res + s[i] = Σ(j=0;i)(s[j]))} ≡ {0 <= i < |s| ^L res = Σ(j=0;i)(s[j]) - s[i]} ≡
{0 <= i < |s| ^L res = Σ(j=0;i-1)(s[j])} ≡ wp(S, I)
QVQ (I ^ B) => wp(S, I) ≡ (0 <= i <= |s| ^L res = Σ(j=0;i-1)(s[j]) ^ i < |s|) => (0 <= i < |s| ^L res = Σ(j=0;i-1)(s[j])) ≡ True
3. QVQ (I ^ ¬B) => Q_c ≡ (0 <= i <= |s| ^L res = Σ(j=0;i-1)(s[j]) ^ i >= |s|) => (res = Σ(j=0;|s|-1)(s[j])) ≡
(i = |s| ^L res = Σ(j=0;i-1)(s[j])) => (res = Σ(j=0;|s|-1)(s[j])) ≡ True

6.f.
fv = |s| - i
4. QVQ (I ^ B ^ v0 = fv) => wp(S, (|s| - i < v0))
wp(i := i + 1, (|s| - i < v0)) ≡ {|s| - i - 1 < v0} ≡ {Q}
wp(res := res + s[i], Q) ≡ {(0 <= i < |s|) ^L (|s| - i - 1 < v0)} ≡ wp(S, (|s| - i < v0))
QVQ (I ^ B ^ v0 = fv) => wp(S, (|s| - i < v0)) ≡ (0 <= i <= |s| ^L res = Σ(j=0;i-1)(s[j]) ^ i < |s| ^ v0 = fv) => ((0 <= i < |s|) ^L (fv < v0 + 1)) ≡ True
5. QVQ (I ^ fv <= 0) => ¬B ≡ (0 <= i <= |s| ^L res = Σ(j=0;i-1)(s[j]) ^ i >= |s|) => (i >= |s|) ≡ True /* fv = |s| - i <= 0 <=> i >= |s| */ 

7.
P_c = {n >= 0 ^ res = 0 ^ i = 0}
Q_c = asegura = {res = Σ(j=0;n-1)(if j%2=0 then j else 0 fi)}
B = (i < n)
S ≡
res := res + i;
i := i + 2;
I = ((0 <= i <= n + 1) ^ i%2=0 ^ res = Σ(j=0;i-1)(if j%2=0 then j else 0 fi))
fv = n - i
Por el teorema de corrección de un ciclo,
1. QVQ P_c => I ≡ (n >= 0 ^ res = 0 ^ i = 0) => ((0 <= i <= n + 1) ^ i%2=0 ^ res = Σ(j=0;i-1)(if j%2=0 then j else 0 fi)) ≡ True
2. QVQ (I ^ B) => wp(S, I)
wp(i := i + 2, I) ≡ {(0 <= i + 2 <= n + 1) ^ (i+2)%2=0 ^ res = Σ(j=0;i+1)(if j%2=0 then j else 0 fi)} ≡
{(0 <= i + 2 <= n + 1) ^ i%2=0 ^ res = Σ(j=0;i+1)(if j%2=0 then j else 0 fi)} ≡ {Q}
wp(res := res + i, Q) ≡ {(0 <= i + 2 <= n + 1) ^ i%2=0 ^ res + i = Σ(j=0;i+1)(if j%2=0 then j else 0 fi)} ≡ wp(S, I)
QVQ (I ^ B) => wp(S, I) ≡ ((0 <= i <= n + 1) ^ i%2=0 ^ res = Σ(j=0;i-1)(if j%2=0 then j else 0 fi) ^ i < n) => ((0 <= i + 2 <= n + 1) ^ i%2=0 ^ res + i = Σ(j=0;i+1)(if j%2=0 then j else 0 fi)) ≡
((0 <= i < n) ^ i%2=0 ^ res = Σ(j=0;i-1)(if j%2=0 then j else 0 fi)) => ((0 <= i + 2 <= n + 1) ^ i%2=0 ^ res + i = Σ(j=0;i+1)(if j%2=0 then j else 0 fi)) ≡
((0 <= i < n) ^ i%2=0 ^ res = Σ(j=0;i-1)(if j%2=0 then j else 0 fi)) => ((-2 <= i < n) ^ i%2=0 ^ res = Σ(j=0;i+1)(if j%2=0 then j else 0 fi) - i) ≡
((0 <= i < n) ^ i%2=0 ^ res = Σ(j=0;i-1)(if j%2=0 then j else 0 fi)) => ((-2 <= i < n) ^ i%2=0 ^ res = Σ(j=0;i)(if j%2=0 then j else 0 fi) - i) ≡
((0 <= i < n) ^ i%2=0 ^ res = Σ(j=0;i-1)(if j%2=0 then j else 0 fi)) => ((-2 <= i < n) ^ i%2=0 ^ res = Σ(j=0;i-1)(if j%2=0 then j else 0 fi)) ≡ True
3. QVQ (I ^ ¬B) => Q_c ≡ ((0 <= i <= n + 1) ^ i%2=0 ^ res = Σ(j=0;i-1)(if j%2=0 then j else 0 fi) ^ i >= n) => (res = Σ(j=0;n-1)(if j%2=0 then j else 0 fi)) ≡
((n <= i <= n + 1) ^ i%2=0 ^ res = Σ(j=0;i-1)(if j%2=0 then j else 0 fi)) => (res = Σ(j=0;n-1)(if j%2=0 then j else 0 fi)) ≡ True /* i es n o n+1, en cualquier caso la sumatoria da lo mismo */
4. QVQ (I ^ B ^ v0 = fv) => wp(S, (n - i < v0))
wp(i := i + 2, (n - i < v0)) ≡ {n - i - 2 < v0}
wp(res := res + i, (n - i - 2 < v0)) ≡ {n - i - 2 < v0)}
QVQ (I ^ B ^ v0 = fv) => wp(S, (n - i < v0)) ≡ ((0 <= i <= n + 1) ^ i%2=0 ^ res = Σ(j=0;i-1)(if j%2=0 then j else 0 fi) ^ i < n ^ v0 = fv) => (n - i - 2 < v0) ≡
((0 <= i <= n + 1) ^ i%2=0 ^ res = Σ(j=0;i-1)(if j%2=0 then j else 0 fi) ^ i < n ^ v0 = fv) => (fv < v0 + 2) ≡ True
5. QVQ (I ^ fv <= 0) => ¬B ≡ ((0 <= i <= n + 1) ^ i%2=0 ^ res = Σ(j=0;i-1)(if j%2=0 then j else 0 fi) ^ i >= n) => (i >= n) ≡ True /* fv = n - i <= 0 <=> i >= n */

8.a.
S ≡
i := 0;
res := 0;
while (i <= n) do
    if (n%i=0) then
        res := res + i
    else
        skip
    endif
    i := i + 1
endwhile;
8.b.
No puede ser demostrado mediante el invariante propuesto:
- Antes del ciclo el invariante requiere i >= 1 y en el programa i comienza en 0.
- Al final del ciclo el inviariante requiere i <= n y en el programa i termina valiendo n + 1.
Con estas consideraciones, el invariante correspondiente al ciclo propuesto es:
I = ((0 <= i <= n+1) ^ res = Σ(j=1;i)(if n%j=0 then j else 0 fi))

9.a.
P_c = {(|s| = |r|) ^ (r = r0) ^ (i = 0)}
Q_c = asegura = {(|s| = |r|) ^L (∀j: Z)((0 <= j < |s|) =>L (s[j] = r[j]))}
B = (i < |s|)
S ≡
r := setAt(r, i, s[i]);
i := i + 1;
9.b.
I = (((0 <= i <= |s|) ^ (|s| = |r|)) ^L (∀j: Z)((0 <= j < i) =>L (s[j] = r[j])))
1. QVQ P_c => I ≡ ((|s| = |r|) ^ (r = r0) ^ (i = 0)) => (((0 <= i <= |s|) ^ (|s| = |r|)) ^L (∀j: Z)((0 <= j < i) =>L (s[j] = r[j]))) ≡ True
2. QVQ (I ^ B) => wp(S, I)
wp(i := i + 1, I) ≡ {((0 <= i + 1 <= |s|) ^ (|s| = |r|)) ^L (∀j: Z)((0 <= j < i + 1) =>L (s[j] = r[j]))} ≡ {Q}
wp(r := setAt(r, i, s[i]), Q) ≡ {(0 <= i < |s|) ^L (((0 <= i + 1 <= |s|) ^ (|s| = |r|)) ^L (∀j: Z)((0 <= j < i + 1) =>L (s[j] = setAt(r, i, s[i])[j])))} ≡
{((0 <= i < |s|) ^ (|s| = |r|)) ^L (∀j: Z)((0 <= j < i + 1) =>L (s[j] = setAt(r, i, s[i])[j]))} ≡
{((0 <= i < |s|) ^ (|s| = |r|)) ^L (∀j: Z)((0 <= j <= i) =>L (s[j] = setAt(r, i, s[i])[j]))} ≡ /* cuando j = i es trivial que se cumple la condición s[j = i] = r[j = i] */
{((0 <= i < |s|) ^ (|s| = |r|)) ^L (∀j: Z)((0 <= j < i) =>L (s[j] = r[j]))} ≡ wp(S, I)
QVQ (I ^ B) => wp(S, I) ≡ (((0 <= i <= |s|) ^ (|s| = |r|)) ^L (∀j: Z)((0 <= j < i) =>L (s[j] = r[j])) ^ (i < |s|)) => (((0 <= i < |s|) ^ (|s| = |r|)) ^L (∀j: Z)((0 <= j < i) =>L (s[j] = r[j]))) ≡ True
3. QVQ (I ^ ¬B) => Q_c ≡ (((0 <= i <= |s|) ^ (|s| = |r|)) ^L (∀j: Z)((0 <= j < i) =>L (s[j] = r[j])) ^ (i >= |s|)) => ((|s| = |r|) ^L (∀j: Z)((0 <= j < |s|) =>L (s[j] = r[j]))) ≡ True /* originalmente propuse un invariante idéntico pero que no pedía (|s| = |r|), y en este punto se me hizo evidente que era necesario - notar además que sin pedir esa condición, el invariante podría indefinirse, y que debería haber llegado a la necesidad de esta condición al tratar de demostrar 1. */
9.c.
fv = |s| - i
4. QVQ (I ^ B ^ v0 = fv) => wp(S, (|s| - i < v0))
wp(i := i + 1, (|s| - i < v0)) ≡ {|s| - i - 1 < v0}
wp(r := setAt(r, i, s[i]), (|s| - i - 1 < v0)) ≡ {|s| - i - 1 < v0}
QVQ (I ^ B ^ v0 = fv) => wp(S, (|s| - i < v0)) ≡ (((0 <= i <= |s|) ^ (|s| = |r|)) ^L (∀j: Z)((0 <= j < i) =>L (s[j] = r[j])) ^ (i < |s|) ^ (v0 = fv)) => (fv < v0 + 1) ≡ True
5. QVQ (I ^ fv <= 0) => ¬B ≡ (((0 <= i <= |s|) ^ (|s| = |r|)) ^L (∀j: Z)((0 <= j < i) =>L (s[j] = r[j])) ^ (|s| - i <= 0)) => (i >= |s|) ≡ True

10.a.
I = (|s|%2=0 ^L (|s|/2-1 <= i <= |s|-1) ^L suma = Σ(j=0;|s|-2-i)(s[j]))
10.b.
fv = i + 1 - |s|/2
10.c.
1. QVQ P_c => I ≡ (|s|%2=0 ^ (i = |s| - 1) ^ (suma = 0)) => (|s|%2=0 ^L (|s|/2-1 <= i <= |s|-1) ^L suma = Σ(j=0;|s|-2-i)(s[j])) ≡ True
2. QVQ (I ^ B) => wp(S, I)
Con S ≡
suma := suma + s[|s|-1-i];
i := i - 1;
wp(i := i - 1, I) ≡ {|s|%2=0 ^L (|s|/2-1 <= i - 1 <= |s|-1) ^L suma = Σ(j=0;|s|-1-i)(s[j])} ≡ {|s|%2=0 ^L (|s|/2 <= i <= |s|) ^L suma = Σ(j=0;|s|-1-i)(s[j])} ≡ {Q}
wp(suma := suma + s[|s|-1-i], Q) ≡ {(0 <= |s|-1-i < |s|) ^L |s|%2=0 ^L (|s|/2 <= i <= |s|) ^L suma + s[|s|-1-i] = Σ(j=0;|s|-1-i)(s[j])} ≡
{(-|s|+1 <= -i < 1) ^L |s|%2=0 ^L (|s|/2 <= i <= |s|) ^L suma = Σ(j=0;|s|-1-i)(s[j]) - s[|s|-1-i]} ≡
{(-1 < i <= |s|-1) ^L |s|%2=0 ^L (|s|/2 <= i <= |s|) ^L suma = Σ(j=0;|s|-2-i)(s[j])} ≡
{(0 <= i <= |s|-1) ^L |s|%2=0 ^L (|s|/2 <= i <= |s|) ^L suma = Σ(j=0;|s|-2-i)(s[j])} ≡ wp(S, I)
QVQ (I ^ B) => wp(S, I) ≡ (|s|%2=0 ^L (|s|/2-1 <= i <= |s|-1) ^L suma = Σ(j=0;|s|-2-i)(s[j]) ^ (i >= |s|/2)) => ((0 <= i <= |s|-1) ^L |s|%2=0 ^L (|s|/2 <= i <= |s|) ^L suma = Σ(j=0;|s|-2-i)(s[j])) ≡ True
3. QVQ (I ^ ¬B) => Q_c ≡ (|s|%2=0 ^L (|s|/2-1 <= i <= |s|-1) ^L suma = Σ(j=0;|s|-2-i)(s[j]) ^ (i < |s|/2)) => (|s|%2=0 ^ (i = |s|/2-1) ^L suma = Σ(j=0;|s|/2-1)(s[j])) ≡ True /* i = |s|/2-1, |s|-2-(|s|/2-1) = |s|/2-1 */ /* obs.: siendo estricto, el primer ^ de Q_c debería ser ^L ya que en caso contrario la división entera podría indefinirse */
4. QVQ (I ^ B ^ v0 = fv) => wp(S, (i + 1 - |s|/2 < v0))
wp(i := i - 1, (i + 1 - |s|/2 < v0)) ≡ {i - |s|/2 < v0}
wp(suma := suma + s[|s|-1-i], (i - |s|/2 < v0)) ≡ {(0 <= |s|-1-i < |s|) ^L (i - |s|/2 < v0)}
QVQ (I ^ B ^ v0 = fv) => wp(S, (i + 1 - |s|/2 < v0)) ≡ (|s|%2=0 ^L (|s|/2-1 <= i <= |s|-1) ^L suma = Σ(j=0;|s|-2-i)(s[j]) ^ (i >= |s|/2) ^ (v0 = fv)) => ((0 <= |s|-1-i < |s|) ^L (i - |s|/2 < v0)) ≡
(|s|%2=0 ^L (|s|/2-1 <= i <= |s|-1) ^L suma = Σ(j=0;|s|-2-i)(s[j]) ^ (i >= |s|/2) ^ (v0 = fv)) => ((0 <= i <= |s|-1) ^L (fv < v0 + 1)) ≡ True
5. QVQ (I ^ fv <= 0) => ¬B ≡ (|s|%2=0 ^L (|s|/2-1 <= i <= |s|-1) ^L suma = Σ(j=0;|s|-2-i)(s[j]) ^ (i <= |s|/2 - 1)) => (i < |s|/2) ≡ True /* i = |s|/2-1 */

11.
P = {True} /* obs.: wp(S, Q) necesariamente debe ser True para la correctitud del programa */
Q = {((r = -1) => (∀k: Z)((0 <= k < |s|) =>L (s[k] != e))) ^ ((r != -1) => ((0 <= r < |s|) ^L (s[r] = e)))}
P_c = {(i = |s| - 1) ^ (j = -1)}
Q_c = {((j = -1) => (∀k: Z)((0 <= k < |s|) =>L (s[k] != e))) ^ ((j != -1) => ((0 <= j < |s|) ^L (s[j] = e)))}
B_c = (i >= 0)
I = ((-1 <= i < |s|) ^L (((j = -1) => (∀k: Z)((i < k < |s|) =>L (s[k] != e))) ^ ((j != -1) => ((i < j < |s|) ^L (s[j] = e)))))
fv = i + 1
wp(r := j, Q) ≡ {((j = -1) => (∀k: Z)((0 <= k < |s|) =>L (s[k] != e))) ^ ((j != -1) => ((0 <= j < |s|) ^L (s[j] = e)))}
Como esta wp es igual a Q_c, Q_c la implica. Por lo tanto, el programa posterior al ciclo es correcto.
Ya tengo lo suficiente como para probar la correctitud del ciclo:
1. QVQ P_c => I ≡ ((i = |s| - 1) ^ (j = -1)) => ((-1 <= i < |s|) ^L (((j = -1) => (∀k: Z)((i < k < |s|) =>L (s[k] != e))) ^ ((j != -1) => ((i < j < |s|) ^L (s[j] = e))))) ≡ True
2. QVQ (I ^ B_c) => wp(S_c, I)
wp(i := i - 1, I) ≡ {(-1 <= i-1 < |s|) ^L (((j = -1) => (∀k: Z)((i-1 < k < |s|) =>L (s[k] != e))) ^ ((j != -1) => ((i-1 < j < |s|) ^L (s[j] = e))))} ≡ {Q1}
wp(if s[i]=e then j:=i else skip endif, Q1) ≡ {(0 <= i < |s|) ^L (((s[i] = e) ^ wp(j := i, Q1)) v ((s[i] != e) ^ wp(skip, Q1)))} ≡
{(0 <= i < |s|) ^L (((s[i] = e) ^ wp(j := i, Q1)) v ((s[i] != e) ^ Q1))}
wp(j := i, Q1) ≡ {(-1 <= i-1 < |s|) ^L (((i = -1) => (∀k: Z)((i-1 < k < |s|) =>L (s[k] != e))) ^ ((i != -1) => ((i-1 < i < |s|) ^L (s[i] = e))))} ≡
{(0 <= i < |s|+1) ^L (((i = -1) => (∀k: Z)((i-1 < k < |s|) =>L (s[k] != e))) ^ ((i != -1) => ((i-1 < i < |s|) ^L (s[i] = e))))} ≡
{(0 <= i < |s|+1) ^L ((i-1 < i < |s|) ^L (s[i] = e))} ≡ {(0 <= i < |s|+1) ^L (i < |s|) ^L (s[i] = e)} ≡ {(0 <= i < |s|) ^L (s[i] = e)}
wp(S_c, I) ≡ wp(if s[i]=e then j:=i else skip endif, Q1) ≡ {(0 <= i < |s|) ^L (((s[i] = e) ^ wp(j := i, Q1)) v ((s[i] != e) ^ Q1))} ≡
{(0 <= i < |s|) ^L (((s[i] = e) ^ ((0 <= i < |s|) ^L (s[i] = e))) v ((s[i] != e) ^ Q1))} ≡ {(0 <= i < |s|) ^L ((s[i] = e) v ((s[i] != e) ^ Q1))} ≡
{(0 <= i < |s|) ^L ((s[i] = e) v ((s[i] != e) ^ (-1 <= i-1 < |s|) ^L (((j = -1) => (∀k: Z)((i-1 < k < |s|) =>L (s[k] != e))) ^ ((j != -1) => ((i-1 < j < |s|) ^L (s[j] = e))))))} ≡
{(0 <= i < |s|) ^L ((s[i] = e) v ((s[i] != e) ^ (((j = -1) => (∀k: Z)((i <= k < |s|) =>L (s[k] != e))) ^ ((j != -1) => ((i < j < |s|) ^L (s[j] = e))))))}
QVQ (I ^ B_c) => wp(S_c, I) ≡ ((-1 <= i < |s|) ^L (((j = -1) => (∀k: Z)((i < k < |s|) =>L (s[k] != e))) ^ ((j != -1) => ((i < j < |s|) ^L (s[j] = e)))) ^ (i >= 0)) => ((0 <= i < |s|) ^L ((s[i] = e) v ((s[i] != e) ^ (((j = -1) => (∀k: Z)((i <= k < |s|) =>L (s[k] != e))) ^ ((j != -1) => ((i < j < |s|) ^L (s[j] = e))))))) ≡
((0 <= i < |s|) ^L (((j = -1) => (∀k: Z)((i < k < |s|) =>L (s[k] != e))) ^ ((j != -1) => ((i < j < |s|) ^L (s[j] = e))))) => ((0 <= i < |s|) ^L ((s[i] = e) v ((s[i] != e) ^ (((j = -1) => (∀k: Z)((i <= k < |s|) =>L (s[k] != e))) ^ ((j != -1) => ((i < j < |s|) ^L (s[j] = e))))))) ≡ True /* q => p v (¬p ^ q) es tautológico */
3. QVQ (I ^ ¬B_c) => Q_c ≡ (((-1 <= i < |s|) ^L (((j = -1) => (∀k: Z)((i < k < |s|) =>L (s[k] != e))) ^ ((j != -1) => ((i < j < |s|) ^L (s[j] = e))))) ^ (i < 0)) => (((j = -1) => (∀k: Z)((0 <= k < |s|) =>L (s[k] != e))) ^ ((j != -1) => ((0 <= j < |s|) ^L (s[j] = e)))) ≡ True /* i = -1 */
4. QVQ (I ^ B_c ^ v0 = fv) => wp(S_c, (i + 1 < v0))
wp(i := i - 1, (i + 1 < v0)) ≡ {i + 1 < v0 + 1} ≡ {Q2}
wp(if s[i]=e then j:=i else skip endif, Q2) ≡ {(0 <= i < |s|) ^L (((s[i] = e) ^ wp(j := i, Q2)) v ((s[i] != e) ^ Q2))}
wp(j := i, Q2) ≡ {Q2}
wp(S_c, (i + 1 < v0)) ≡ wp(if s[i]=e then j:=i else skip endif, Q2) ≡ {(0 <= i < |s|) ^L Q2} ≡ {(0 <= i < |s|) ^L (i + 1 < v0 + 1)}
QVQ (I ^ B_c ^ v0 = fv) => wp(S_c, (i + 1 < v0)) ≡ ((-1 <= i < |s|) ^L (((j = -1) => (∀k: Z)((i < k < |s|) =>L (s[k] != e))) ^ ((j != -1) => ((i < j < |s|) ^L (s[j] = e)))) ^ (i >= 0) ^ (v0 = fv)) => ((0 <= i < |s|) ^L (fv < v0 + 1)) ≡ True
5. QVQ (I ^ fv <= 0) => ¬B_c ≡ (((-1 <= i < |s|) ^L (((j = -1) => (∀k: Z)((i < k < |s|) =>L (s[k] != e))) ^ ((j != -1) => ((i < j < |s|) ^L (s[j] = e))))) ^ (i <= -1)) => (i < 0) ≡ True /* i = -1 */
El ciclo termina y es correcto.
Basta ver que P = {True} => wp(i := |s| - 1, wp(j := -1, P_c))
wp(i := |s| - 1, wp(j := -1, P_c)) ≡ wp(i := |s| - 1, wp(j := -1, ((i = |s| - 1) ^ (j = -1)))) ≡ wp(i := |s| - 1, ((i = |s| - 1) ^ (-1 = -1))) ≡
wp(i := |s| - 1, (i = |s| - 1)) ≡ {|s| - 1 = |s| - 1} ≡ {True}
P => wp(i := |s| - 1, wp(j := -1, P_c)) ≡ True => True ≡ True
Por el corolario de monotonía todo el programa es correcto.

12.
P = {True} /* obs.: wp(S, Q) necesariamente debe ser True para la correctitud del programa */
Q = {res = True <=> (∃k: Z)((0 <= k < |s|) ^L (s[k] = e))}
P_c = {(i = 0) ^ (j = -1)}
B_c = (i < |s|)
I = ((0 <= i <= |s|) ^L ((j != -1) <=> (∃k: Z)((0 <= k < i) ^L (s[k] = e))))
fv = |s| - i
Q_c = {(j != -1) <=> (∃k: Z)((0 <= k < |s|) ^L (s[k] = e))}
wp(if j!=-1 then res:=true else res:=false endif, Q) ≡ {((j != -1) ^ wp(res := True, Q)) v ((j = -1) ^ wp(res := False, Q))}
wp(res := True, Q) ≡ {True = True <=> (∃k: Z)((0 <= k < |s|) ^L (s[k] = e))} ≡ {(∃k: Z)((0 <= k < |s|) ^L (s[k] = e))}
wp(res := False, Q) ≡ {False = True <=> (∃k: Z)((0 <= k < |s|) ^L (s[k] = e))} ≡ {¬(∃k: Z)((0 <= k < |s|) ^L (s[k] = e))}
wp(if j!=-1 then res:=true else res:=false endif, Q) = {((j != -1) ^ (∃k: Z)((0 <= k < |s|) ^L (s[k] = e))) v ((j = -1) ^ ¬(∃k: Z)((0 <= k < |s|) ^L (s[k] = e)))} ≡
{(j != -1) <=> (∃k: Z)((0 <= k < |s|) ^L (s[k] = e))}
Como esta wp es igual a Q_c, Q_c la implica. Por lo tanto, el programa posterior al ciclo es correcto.
Ya tengo lo suficiente como para probar la correctitud del ciclo:
1. QVQ P_c => I ≡ ((i = 0) ^ (j = -1)) => ((0 <= i <= |s|) ^L ((j != -1) <=> (∃k: Z)((0 <= k < i) ^L (s[k] = e)))) ≡ True
2. QVQ (I ^ B_c) => wp(S_c, I)
wp(i := i + 1, I) ≡ {(0 <= i+1 <= |s|) ^L ((j != -1) <=> (∃k: Z)((0 <= k < i+1) ^L (s[k] = e)))} ≡ {Q1}
wp(if s[i]=e then j:=i else skip endif, Q1) ≡ {(0 <= i < |s|) ^L (((s[i] = e) ^ wp(j := i, Q1)) v ((s[i] != e) ^ wp(skip, Q1)))}
wp(j := i, Q1) ≡ {(0 <= i+1 <= |s|) ^L ((i != -1) <=> (∃k: Z)((0 <= k < i+1) ^L (s[k] = e)))}
wp(S_c, I) ≡ wp(if s[i]=e then j:=i else skip endif, Q1) ≡ {(0 <= i < |s|) ^L (((s[i] = e) ^ wp(j := i, Q1)) v ((s[i] != e) ^ Q1))} ≡
{(0 <= i < |s|) ^L (((s[i] = e) ^ ((0 <= i+1 <= |s|) ^L ((i != -1) <=> (∃k: Z)((0 <= k < i+1) ^L (s[k] = e))))) v ((s[i] != e) ^ ((0 <= i+1 <= |s|) ^L ((j != -1) <=> (∃k: Z)((0 <= k < i+1) ^L (s[k] = e))))))} ≡
{(0 <= i < |s|) ^L (((s[i] = e) ^ (∃k: Z)((0 <= k < i+1) ^L (s[k] = e))) v ((s[i] != e) ^ ((j != -1) <=> (∃k: Z)((0 <= k < i+1) ^L (s[k] = e)))))} ≡
{(0 <= i < |s|) ^L (True v ((s[i] != e) ^ ((j != -1) <=> (∃k: Z)((0 <= k < i+1) ^L (s[k] = e)))))} ≡ {0 <= i < |s|}
QVQ (I ^ B_c) => wp(S_c, I) ≡ ((0 <= i <= |s|) ^L ((j != -1) <=> (∃k: Z)((0 <= k < i) ^L (s[k] = e))) ^ (i < |s|)) => (0 <= i < |s|) ≡ True
3. QVQ (I ^ ¬B) => Q_c ≡ ((0 <= i <= |s|) ^L ((j != -1) <=> (∃k: Z)((0 <= k < i) ^L (s[k] = e))) ^ (i >= |s|)) => ((j != -1) <=> (∃k: Z)((0 <= k < |s|) ^L (s[k] = e))) ≡ True /* i = |s| */
4. QVQ (I ^ B_c ^ v0 = fv) => wp(S_c, (|s| - i < v0))
wp(i := i + 1, (|s| - i < v0)) ≡ {|s| - i < v0 + 1} ≡ {Q2}
wp(if s[i]=e then j:=i else skip endif, Q2) ≡ {(0 <= i < |s|) ^L (((s[i] = e) ^ wp(j := i, Q2)) v ((s[i] != e) ^ Q2))}
wp(j := i, Q2) ≡ {Q2}
wp(S_c, (|s| - i < v0)) ≡ wp(if s[i]=e then j:=i else skip endif, Q2) ≡ {(0 <= i < |s|) ^L Q2} ≡ {(0 <= i < |s|) ^L (|s| - i < v0 + 1)}
QVQ (I ^ B_c ^ v0 = fv) => wp(S_c, (|s| - i < v0)) ≡ ((0 <= i <= |s|) ^L ((j != -1) <=> (∃k: Z)((0 <= k < i) ^L (s[k] = e))) ^ (i < |s|) ^ (v0 = fv)) => ((0 <= i < |s|) ^L (fv < v0 + 1)) ≡ True
5. QVQ (I ^ fv <= 0) => ¬B_c ≡ ((0 <= i <= |s|) ^L ((j != -1) <=> (∃k: Z)((0 <= k < i) ^L (s[k] = e))) ^ (|s| - i <= 0)) => (i >= |s|) ≡ True /* i = |s| */
El ciclo termina y es correcto.
Basta ver que P = {True} => wp(i := 0, wp(j := -1, P_c))
wp(i := 0, wp(j := -1, P_c)) ≡ wp(i := 0, ((i = 0) ^ (-1 = -1))) ≡ {(0 = 0) ^ True} ≡ {True}
P => wp(i := 0, wp(j := -1, P_c)) ≡ True => True ≡ True
Por el corolario de monotonía todo el programa es correcto.

13.
P = {(|r| = |a| + |b|) ^ (r = r0)}
Q = {(|r| = |r0|) ^L ((∀j: Z)((0 <= j < |a|) =>L (r[j] = a[j])) ^ (∀j: Z)((0 <= j < |b|) =>L (r[j + |a|] = b[j])))} /* obs.: siendo estricto, el primer ^ debería ser ^L */
P_c1 = {(|r| = |a| + |b|) ^ (r = r0) ^ (i = 0)}
P_c2 = {Q_c1 ^ (i = 0)}
Para poder demostrar la correctitud del segundo ciclo necesito P_c2, por lo tanto necesito Q_c1, pero no lo tengo.
Entonces, propongo que Q_c1 es la primera parte del asegura, Q:
Q_c1 = {(|r| = |r0|) ^L (∀j: Z)((0 <= j < |a|) =>L (r[j] = a[j]))} /* me genera dudas si es necesario incluir |r| = |r0|, sospecho que lo és */
Q_c2 = {Q}
B_c1 = (i < |a|)
B_c2 = (i < |b|)
fv_c1 = |a| - i
fv_c2 = |b| - i
I_c1 = (((0 <= i <= |a|) ^ (|r| = |r0|)) ^L (∀j: Z)((0 <= j < i) =>L (r[j] = a[j])))
I_c2 = ((Q_c1 ^ (0 <= i <= |b|)) ^L (∀j: Z)((0 <= j < i) =>L (r[j + |a|] = b[j])))
Ya tengo lo suficiente como para probar la correctitud del segundo ciclo:
c2.1. QVQ P_c2 => I_c2 ≡ (Q_c1 ^ (i = 0)) => ((Q_c1 ^ (0 <= i <= |b|)) ^L (∀j: Z)((0 <= j < i) =>L (r[j + |a|] = b[j]))) ≡ True
c2.2. QVQ (I_c2 ^ B_c2) => wp(S_c2, I_c2)
wp(S_c2, I_c2) ≡ wp(r := setAt(r, |a|+i, b[i]), wp(i := i + 1, I_c2))
wp(i := i + 1, I_c2) ≡ {(Q_c1 ^ (0 <= i+1 <= |b|)) ^L (∀j: Z)((0 <= j < i+1) =>L (r[j + |a|] = b[j]))}
wp(S_c2, I_c2) ≡ {((0 <= |a|+i < |r|) ^ (0 <= i < |b|)) ^L ((Q_c1 ^ (0 <= i+1 <= |b|)) ^L (∀j: Z)((0 <= j < i+1) =>L (setAt(r, |a|+i, b[i])[j + |a|] = b[j])))} ≡ /* Q_c1 no se ve afectado por el cambio sobre r */
{((0 <= |a|+i < |r|) ^ (0 <= i < |b|)) ^L (Q_c1 ^L (∀j: Z)((0 <= j <= i) =>L (setAt(r, |a|+i, b[i])[j + |a|] = b[j])))} ≡ /* si j = i, es trivial que se cumple la condición del para todo */
{((0 <= |a|+i < |r|) ^ (0 <= i < |b|)) ^L (Q_c1 ^L (∀j: Z)((0 <= j < i) =>L (r[j + |a|] = b[j])))}
QVQ (I_c2 ^ B_c2) => wp(S_c2, I_c2) ≡ ((Q_c1 ^ (0 <= i <= |b|)) ^L (∀j: Z)((0 <= j < i) =>L (r[j + |a|] = b[j])) ^ (i < |b|)) => (((0 <= |a|+i < |r|) ^ (0 <= i < |b|)) ^L (Q_c1 ^L (∀j: Z)((0 <= j < i) =>L (r[j + |a|] = b[j])))) ≡ True /* (0 <= |a|+i < |r|) es True porque por Q_c1 |r| = |r0| = |a| + |b| sumado a que (i < |b|) */
c2.3. QVQ (I_c2 ^ ¬B_c2) => Q_c2 ≡ ((Q_c1 ^ (0 <= i <= |b|)) ^L (∀j: Z)((0 <= j < i) =>L (r[j + |a|] = b[j])) ^ (i >= |b|)) => (Q_c1 ^L (∀j: Z)((0 <= j < |b|) =>L (r[j + |a|] = b[j]))) ≡ True /* i = |b| */
c2.4. QVQ (I_c2 ^ B_c2 ^ v0 = fv_c2) => wp(S_c2, (|b| - i < v0))
wp(S_c2, (|b| - i < v0)) ≡ wp(r := setAt(r, |a|+i, b[i]), wp(i := i + 1, (|b| - i < v0))) ≡ wp(r := setAt(r, |a|+i, b[i]), (|b| - i < v0 + 1)) ≡ {fv_c2 < v0 + 1}
QVQ (I_c2 ^ B_c2 ^ v0 = fv_c2) => wp(S_c2, (|b| - i < v0)) ≡ ((Q_c1 ^ (0 <= i <= |b|)) ^L (∀j: Z)((0 <= j < i) =>L (r[j + |a|] = b[j])) ^ (i < |b|) ^ (v0 = fv_c2)) => (fv_c2 < v0 + 1) ≡ True
c2.5. QVQ (I_c2 ^ fv_c2 <= 0) => ¬B_c2 ≡ ((Q_c1 ^ (0 <= i <= |b|)) ^L (∀j: Z)((0 <= j < i) =>L (r[j + |a|] = b[j])) ^ (|b| <= i)) => (i >= |b|) ≡ True /* i = |b| */
Para probar la correctitud del primer ciclo, primero tengo que ver que es cierto que Q_c1 => wp(i := 0, P_c2) ≡ Q_c1 => (Q_c1 ^ (0 = 0)) ≡ True
Ya tengo lo suficiente como para probar la correctitud del primer ciclo:
c1.1. QVQ P_c1 => I_c1 ≡ ((|r| = |a| + |b|) ^ (r = r0) ^ (i = 0)) => (((0 <= i <= |a|) ^ (|r| = |r0|)) ^L (∀j: Z)((0 <= j < i) =>L (r[j] = a[j]))) ≡ True
c1.2. QVQ (I_c1 ^ B_c1) => wp(S_c1, I_c1)
wp(S_c1, I_c1) ≡ wp(r := setAt(r, i, a[i]), wp(i := i + 1, I_c1))
wp(i := i + 1, I_c1)) ≡ {((0 <= i+1 <= |a|) ^ (|r| = |r0|)) ^L (∀j: Z)((0 <= j < i+1) =>L (r[j] = a[j]))}
wp(S_c1, I_c1) ≡ {((0 <= i < |r|) ^ (0 <= i < |a|)) ^L (((0 <= i+1 <= |a|) ^ (|setAt(r, i, a[i])| = |r0|)) ^L (∀j: Z)((0 <= j < i+1) =>L (setAt(r, i, a[i])[j] = a[j])))} ≡
{((0 <= i < |r|) ^ (0 <= i < |a|)) ^L (((-1 <= i < |a|) ^ (|r| = |r0|)) ^L (∀j: Z)((0 <= j < i+1) =>L (setAt(r, i, a[i])[j] = a[j])))} ≡
{((0 <= i < |r|) ^ (0 <= i < |a|) ^ (|r| = |r0|)) ^L (∀j: Z)((0 <= j < i) =>L (r[j] = a[j]))}
QVQ (I_c1 ^ B_c1) => wp(S_c1, I_c1) ≡ (((0 <= i <= |a|) ^ (|r| = |r0|)) ^L (∀j: Z)((0 <= j < i) =>L (r[j] = a[j])) ^ (i < |a|)) => (((0 <= i < |r|) ^ (0 <= i < |a|) ^ (|r| = |r0|)) ^L (∀j: Z)((0 <= j < i) =>L (r[j] = a[j]))) ≡ True
c1.3. QVQ (I_c1 ^ ¬B_c1) => Q_c1 ≡ (((0 <= i <= |a|) ^ (|r| = |r0|)) ^L (∀j: Z)((0 <= j < i) =>L (r[j] = a[j])) ^ (i >= |a|)) => ((|r| = |r0|) ^L (∀j: Z)((0 <= j < |a|) =>L (r[j] = a[j]))) ≡ True /* i = |a| */
c1.4. QVQ (I_c1 ^ B_c1 ^ v0 = fv_c1) => wp(S_c1, (|a| - i < v0))
wp(S_c1, (|a| - i < v0)) ≡ wp(r := setAt(r, i, a[i]), wp(i := i + 1, (|a| - i < v0))) ≡ wp(r := setAt(r, i, a[i]), (|a| - i < v0 + 1)) ≡ {fv_c1 < v0 + 1}
QVQ (I_c1 ^ B_c1 ^ v0 = fv_c1) => wp(S_c1, (|a| - i < v0)) ≡ (((0 <= i <= |a|) ^ (|r| = |r0|)) ^L (∀j: Z)((0 <= j < i) =>L (r[j] = a[j])) ^ (i < |a|) ^ (v0 = fv_c1)) => (fv_c1 < v0 + 1) ≡ True
c1.5. QVQ (I_c1 ^ fv_c1 <= 0) => ¬B_c1 ≡ (((0 <= i <= |a|) ^ (|r| = |r0|)) ^L (∀j: Z)((0 <= j < i) =>L (r[j] = a[j])) ^ (|a| <= i)) => (i >= |a|) ≡ True /* i = |a| */
Solo queda ver que P => wp(i := 0, P_c1) ≡ P => ((|r| = |a| + |b|) ^ (r = r0) ^ (0 = 0)) ≡ P => P ≡ True
Por el corolario de monotonía todo el programa es correcto.