tengo una duda con respecto a la lógica de Hoare que no se muy bien como aplicarla. Supongamos que tenemos dos ciclos whiles con una condición B1 y B2; instrucciones S1 y S2
while B1:
while B2:
S2
S1
Y luego tengo los invariantes I1 e I2 Ahora supongamos que pruebo el teorema del invariante para while 2 y la tripla es válida, entonces la precondición del while 2 implica el I2
Ahora una vez que se eso me quedan las siguientes triplas:
{Pc1}
While B1:
{Pc2}
While B2:
S2
{Qc2}
S2
{Qc1}
Para la instrucción S2 puedo sacar la weakest precondition wp(S2,Qc1) y probar correctitud pero el while 2 no
Porque no existe una weakest precondition cerrada.
Si quiero por ejemplo probar la siguiente tripla de Hoare
{I1 ^ B1} while B2 do..endwhile; S2 {I1}
Tengo que probar que
I1 ^ B1 => wp(while B2 do .. endwhile; S2, I1)
Y lo que conozco es que
Pc2 => wp(while B2 do .. endwhile, Qc2)
como se probaria habiendo probado el ciclo interno?