Title 2. Reglas de correctitud de algoritmos.pdf ✅

1 Reglas de correctitud de algoritmos. Diseñado por: David Díaz Reglas de corrección Tripleta de Hoare: La tripleta de Hoare tiene la siguiente forma {P} S {Q} Donde P es la precondición, S es un programa y Q es la postcondición. Lo que significa es que si la instrucción S se ejecuta en cualquier estado que satisfaga P, entonces se satisface Q después de la ejecución de la instrucción S. Teoremas Teorema 1.a Fortalecimiento de la precondición Si se tiene un teorema P0 ⇒ P, entonces {P} S {Q} También se puede utilizar como {P0 } S {Q} Teorema 1.b Debilitamiento de la postcondición Si se tiene un teorema Q ⇒ Q0, entonces {P} S {Q} También se puede utilizar como {P} S {Q0 } Teorema 2 Evitando un no estado {P} S {false} ≡ (P ≡ false) Significa que no existe ninguna precondición posible que a través de la instrucción S sea capaz de hacer que false sea cierto.
2 Reglas de correctitud de algoritmos. Diseñado por: David Díaz Teorema 3 Regla de la conjunción {P} S {Q} ∧ {P} S {R} ⇒ {P} S {Q ∧ R} Teorema 4 Regla de la disyunción {P} S {Q} ∧ {R} S {Q} ⇒ {P ∨ R} S {Q} Precondición más débil: Conseguir la precondición más débil es conseguir la precondición menos precisa que hace cumplir la tripleta de Hoare {P} S {Q} Con la menos precisa nos referimos a aquella que permite la mayor cantidad de estados iniciales que cumplen la tripleta. Se escribe como wp. S. Q, haciendo referencia a que es la precondición más débil que hace cumplir Q a través de la instrucción S. Es importante notar que la precondición más débil depende la instrucción S, así que habrá una precondición más débil para cada instrucción en GCL. Como wp. S.Q es la precondición más débil, entonces cualquier P que cumpla {P} S {Q} es más preciso que wp. S.Q y; por lo tanto: P ⇒ wp. S. Q
3 Reglas de correctitud de algoritmos. Diseñado por: David Díaz Reglas de correctitud y precondición más débil de cada instrucción: Skip: Regla de correctitud del skip: {P} skip {Q} ≡ P ⇒ Q El skip es interpretado como una implicación porque, por definición, skip no hace nada. Entonces, para demostrar que a partir de la precondición P se puede llegar a la postcondición Q sin hacer nada en la instrucción que las relaciona, entonces esto es simplemente demostrar que P puede implicar Q (P ⇒ Q) Precondición más débil del skip: Si se tiene la siguiente tripleta de Hoare, {P} skip {Q} note que la precondición que es cierta en más estados iniciales (o la menos precisa) es simplemente Q, porque la tripleta es correcta si P ⇒ Q, ahora si P ≡ Q, se tiene Q ⇒ Q es la precondición que tiene más estados iniciales que la hace cierta (la menos precisa). Así, la precondición más débil del skip es wp. skip. Q ≡ Q [ {P} skip {Q} ]