Tiêu đề 3. Reglas de iteración y práctica.pdf ✅

1 Regla de corrección de iteración. Regla de iteración Ahora que ya sabemos cómo demostrar la correctitud de las instrucciones, tan solo nos queda demostrar la correctitud de la iteración (o sea, el do). Para poder llegar a demostrar que la iteración en efecto es correcta, debemos primero entender algunos conceptos de la misma. Invariante Es aquella condición que siempre es cierta mientras se ejecuta una iteración, incluso cuando la iteración está por terminar. Es decir, es una expresión booleana que evalúa a true en todas las instancias de la iteración (para todas las veces que se ejecuta la iteración) Para entender el invariante es necesario ver un ejemplo: Note que una condición que no varía en cualquier instancia de la iteración podría ser x ≥ 0, que es cierto en cada una de las veces que se ejecuta el do, incluso cuando está por terminar. Otra posible condición que se cumple siempre es: 6 ≥ x ≥ 0, que es una condición más fuerte, más precisa. A estas condiciones que se cumplen para todas las iteraciones del bucle de le conoce como el invariante. Y en las demostraciones se denota con la letra P. En un momento volveremos con más ejemplos de invariantes. Cota: La cota es un recurso que se utiliza en las demostraciones para garantizar que tu bucle en algún momento terminará de ejecutarse y no se quedará en un bucle infinito. La cota se define como “una función entera que está acotada por debajo y que decrece con cada iteración”. La función de cota simplemente va a ser una función que nos ayude a garantizar que la iteración va a ir tendiendo a terminar su ejecución. [ var x ∶ Z; ሼx = 0ሽ do x ≤ 5 → x ≔ x + 1; od ሼx > 0ሽ ]
2 Regla de corrección de iteración. La función de cota la denotaremos con la letra t en las demostraciones. La función de cota podría ser: t(x) = N − x Fíjese que x a medida que x va aumentando, N − x va disminuyendo. Es decir, por cada iteración del do, t(x) se va haciendo más pequeña. Pero además t(x) está acotada por debajo, porque N − x > 0 Fíjese que no existirá forma de que cuando x crezca supere a N porque se termina la iteración cuando x = N. Elementos de la regla de iteración: Ahora que sabemos qué es el invariante y qué es la función de cota, vamos a analizar la regla de iteración: Se tiene una iteración de la siguiente forma: Lo primero que debemos entender es que cuando alguna de las guardias no se cumpla, entonces el programa tiene que seguir funcionando, a diferencia de la selección, este no aborta, sino que hace cumplir la postcondición. Es decir, cuando ninguna guardia se cumpla es porque el programa terminó y la postcondición se debería cumplir. De ahí sale el primer ítem: i) P ∧ ¬B0 ∧ ¬B1 ⇒ Q Se incluye el invariante porque recordemos que el invariante se cumple siempre en la iteración. [ const N ∶ Z; var x ∶ Z; ሼN > 0 ∧ x = 0ሽ do x < N → x ≔ x + 1; od ሼx > 0ሽ ] [ ሼInvariante: P , Cota: tሽ do B0 → S0; [ ] B1 → S1; od ሼQሽ ]
3 Regla de corrección de iteración. Con respecto al invariante, recuerde que por cada iteración del bucle el invariante se tiene que cumplir de nuevo. Es decir, cada vez que pase una iteración del bucle, se debería volver a cumplir el invariante. Entonces, eso nos deja el siguiente ítem: ii) ሼP ∧ B0 ሽ S0 ሼPሽ iii) ሼP ∧ B1 ሽ S1 ሼPሽ Y claro, es evidente que cumplido el invariante y cualquier guardia, a través de la instrucción, debe cumplirse de nuevo el invariante. Recordando que el invariante es una condición que se cumple siempre durante la ejecución del bucle. Así, tendríamos los tres ítems relacionados con el invariante: i) P ∧ ¬B0 ∧ ¬B1 ⇒ Q ii) ሼP ∧ B0 ሽ S0 ሼPሽ iii) ሼP ∧ B1 ሽ S1 ሼPሽ Ahora debemos ir con las demostraciones relacionadas con la función de cota. Estas también salen de la definición de la misma función de cota. La función de cota tiene que estar acotada por debajo. Para hacer el mecanismo más sencillo vamos a generalizar que la función estará acotada por debajo por el número 0. Es decir, para demostrar que está acotada por debajo, demostraremos que en el bucle la función de cota es mayor o igual que cero. i) P ∧ (B0 ∨ B1 ) ⇒ t ≥ 0 Es decir, que siempre que estemos en el bucle la cota será mayor o igual que cero. Note que P ∧ (B0 ∨ B1 ) simplemente significa que estamos en el bucle porque se cumple el invariante y cualquiera de las dos guardias. Luego, debemos demostrar que la función de cota está decreciendo. Esto lo garantizamos demostrando que, si la función de cota entra con algún valor en las guardias y ejecuta la instrucción, al final la función de cota va a tener un valor menor que con el que entró. ii) ሼP ∧ B0 ∧ t = Cሽ S0 ሼt < Cሽ iii) ሼP ∧ B1 ∧ t = Cሽ S1 ሼt < Cሽ
4 Regla de corrección de iteración. Finalmente, para demostrar una iteración Debo demostrar: i) P ∧ ¬B0 ∧ ¬B1 ⇒ Q ii) ሼP ∧ B0 ሽ S0 ሼPሽ iii) ሼP ∧ B1 ሽ S1 ሼPሽ Función de cota: i) P ∧ (B0 ∨ B1 ) ⇒ t ≥ 0 ii) ሼP ∧ B0 ∧ t = Cሽ S0 ሼt < Cሽ iii) ሼP ∧ B1 ∧ t = Cሽ S1 ሼt < Cሽ [ ሼInvariante: P , Cota: tሽ do B0 → S0; [ ] B1 → S1; od ሼQሽ ]