0

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?

2
  • hummm ... {Pc2} es la precondicion del ciclo interno, recuerda que el teorema de hoare se aplica de manera iterativa. Commented el 19 feb. a las 20:25
  • entonces se aplica la invariante: {I1 ^ Pc2} Commented el 19 feb. a las 20:26

0

Tu Respuesta

By clicking “Publica tu respuesta”, you agree to our terms of service and acknowledge you have read our privacy policy.

Examina otras preguntas con la etiqueta o formula tu propia pregunta.