El invariante del bucle en el procedimiento para demostrar la exactitud de bucle puede parecer como un conejo en un sombrero. ¿De dónde viene? El h...

El invariante del bucle en el procedimiento para demostrar la exactitud de bucle puede parecer como un conejo en un sombrero. ¿De dónde viene? El hecho es que el desarrollo de un invariante del bucle bueno es un proceso difícil. Aunque el aprendizaje de cómo hacer está más allá del alcance de este libro, vale la pena hacerlo en un curso más avanzado. Las personas que han llegado a ser buenas en el proceso de exactitud han modificado de manera significativa sus perspectivas acerca de programación y han mejorado mucho su capacidad de escribir un buen código. Otro aspecto difícil al manejar pruebas de exactitud se debe al hecho de que la ejecución de un algoritmo es un proceso dinámico, que se realiza en el tiempo. Conforme progresa la ejecución, los valores de las variables van cambiando, aunque a menudo sus nombres no cambian. En el análisis siguiente, cuando necesitamos hacer una distinción entre los valores de una variable justo antes de la ejecución de una frase del algoritmo y justo después de la ejecución de la frase, adjuntaremos los subíndices viejo y nuevo en el nombre de la variable. Ejemplo 5.5.2 Exactitud de un bucle para calcular un producto El siguiente bucle está diseñado para calcular el producto mx para un entero no negativo m y un número real x, sin utilizar una operación de multiplicación incorporada. Antes del bucle, las variables i y productos se han introducido y dan los valores iniciales de i 0 y producto 0. [Pre-condición: m es un entero no negativo, x es un número real, i 0 y el producto 0.] while (i = m) 1. producto: producto x 2. i : i 1 end while [Post-condición: producto mx] Sea el invariante del bucle I (n): i n y el producto nx La condición de guarda G del bucle while es G: i = m Utilice el teorema del invariante del bucle para probar que el bucle while es correcto con respecto a la propuesta de las pre y post-condiciones. Solución I. Propiedad básica: [I(0) es verdadero antes de la primera iteración del bucle.] I(0) es “i 0 y el producto 0 x”, que es verdadero antes de la primera iteración del bucle porque 0 x 0. II. Propiedad inductiva: [Si G I(k) es verdadero antes de una iteración de bucle (donde k 0), entonces I(k 1) es verdadero después de la iteración del bucle.] Supongamos que k es un entero no negativo de tal manera que G I(k) es verdadera antes de una iteración del bucle. Entonces, cuando la ejecución llega a la parte superior del bucle, i = m, producto kx, e i k. Ya que i = m, se pasa la guarda y se ejecuta el enunciado. Antes de la ejecución del enunciado 1, productoviejo kx. Por tanto la ejecución del enunciado 1 tiene el siguiente efecto: productonuevo productoviejo x kx x (k 1)x. Del mismo modo, antes de que se ejecute el enunciado 2, iviejo k, así después de la ejecución del enunciado 2, inuevo iviejo 1 k 1. Por tanto, después de la iteración del bucle, el enunciado I(k 1), a saber, (i k 1 y producto (k 1)x), es verdadero. Esto es lo que necesita demostrar. III. Posible falsedad de la guarda: [Después de un número finito de iteraciones del bucle, G se convierte en falso.] El guarda G es la condición i = m y m es un entero no negativo. Por I y II, se sabe que para todo entero n 0, si el bucle se itera n veces, entonces i n y el producto nx. Así después de m iteraciones del bucle, i m. Por tanto G se convierte en falsa después de m iteraciones del bucle. IV. Exactitud de la post-condición: [Si N es el número menor de iteraciones después de lo que G es falsa e I(N) es verdadera, entonces el valor de las variables del algoritmo será tal como se especifica en la post-condición del bucle.] De acuerdo con la post-condición, el valor de producto después de la ejecución del bucle debe ser mx. Pero si G se convierte en falsa después de N iteraciones, i m. Y si I(N) es verdadera, i N y producto Nx. Puesto que ambas condiciones (G falsa e I(N), verdadera) se satisfacen, m i N y producto mx cuando sea necesario. En lo que resta de esta sección, se presentan pruebas de la exactitud de los bucles fundamentales en el algoritmo de la división y en el algoritmo de Euclides. (Estos algoritmos se presentaron en la sección 4.8.) Exactitud del algoritmo de división El algoritmo de la división se supone que debe tener un número entero no negativo y un en te ro positivo d y calcula los enteros no negativos q y r tales que a dq r y 0 r d. Inicialmente se introducen las variables r y q y se dan los valores r a y q 0. El bu cle crucial, con las pre y las post-condiciones escritas, es la siguiente: [Pre-condición: a es un entero no negativo y d es un entero positivo, r a y q 0.] while (r d) l. r : r ฀ d 2. q : q 1 end while [Post-condición: q y r son números enteros no negativos con la propiedad de que a qd r y 0 r d.] Demostración: Para demostrar la exactitud del bucle, sea el invariante del bucle I (n): r a ฀ nd 0 y n q. El guarda del bucle while es G: r d I. Propiedad básica: [I(0) es verdadera antes de la primera iteración del bucle.] I(0) es “r a ฀ 0 d 0 y q 0”. Pero por la precondición, r a, a 0 y q 0. Por lo que ya que a a ฀ 0 d, entonces r a ฀ 0 d y I(0) es verdadera antes de la primera iteración del bucle. II. Propiedad inductiva: [Si G I(k) es verdadera antes de una iteración del bucle (donde k 0), I (k 1) es verdadera después de la iteración del bucle.] Supongamos que k es un entero no negativo tal que G I (k) es verdadera antes de una iteración del bucle. Puesto que G es verdadera, r d y se introduce el bucle. También puesto que I (k) es verdadero, r a ฀ kd 0 y k q. Por tanto, antes de la ejecución de los enunciados 1 y 2, rviejo d y rviejo a ฀ kd y qviejo k. Cuando se ejecutan los enunciados 1 y 2, entonces, rnuevo rviejo ฀ d (a ฀ kd) ฀ d a ฀ (k 1)d, 5.5.2 y qnuevo qviejo 1 k l 5.5.3 Además ya que rviejo d antes de la ejecución de los enunciados 1 y 2, después de la ejecución de estos enunciados, rnuevo O y rnuevo a ฀ (k 1)d y qnuevo k 1. Por tanto I (k 1) es verdadera. III. Posible falsedad de la guarda: [Después de un número finito de iteraciones del bucle, G se convierte en falsa.] El guarda G es la condición r d. Cada iteración del bucle reduce el valor de r por d y sin embargo deja a r no negativo. Por tanto los valores de r forman una sucesión decreciente de números enteros no negativos y así (por el principio del buen orden) debe haber el más pequeño r como, por ejemplo rmín. Entonces rmín d. [Si rmín fuera mayor que d, el bucle se itera en otra ocasión y se obtendría un nuevo valor de r igual a rmín ฀ d. Pero este nuevo valor sería menor que rmín que estaría en contradicción con el hecho de que rmín es el residuo más pequeño obtenido por iteración repetida del bucle.] Por tanto, tan pronto como el valor de r rmín, se calcula el valor de r y se convierte menor que d, por lo que el guarda de G es falsa. IV. Exactitud de la post-condición: [Si N es el menor número de iteraciones después de que G es falsa e I (N) es verdadera