Hoare Logic Loop Invariant

Question

Estoy mirando Hoare Logic y tengo problemas para entender el método de búsqueda del bucle invariante.

¿Alguien puede explicar el método utilizado para calcular el bucle invariante?

¿Y qué debe contener un bucle invariante para ser "útil"?

Sólo estoy tratando con ejemplos simples, la búsqueda de invariantes y demostrando corrección parcial y completa en ejemplos como:

{ i ≥ 0 } while i > 0 do i := i−1 { i = 0 } 

Answer 1

Si estamos hablando de la Lógica de Hoare para probar la corrección (parcial) de los programas, a continuación, utiliza la condición previa y condición posterior, descomponer el programa y utilizar las reglas del sistema de inferencia lógica de Hoare para crear y probar una fórmula inductivo.

En su ejemplo, que desea descomponer el programa usando la regla

{p} while b do S {p^not(b)} <=> {p^b} S {p} 

En su caso

• t: i ≥ 0
• b: i> 0
• S: i: = i-1.

En el siguiente paso inferimos {i ≥ 0^i > 0} i := i−1 {i ≥ 0}. Esto se puede inferir y probar con bastante facilidad. Espero que esto ayude.

Answer 2

ser útil (por su razonamiento) es el punto principal de la invariante. Por lo tanto, observe la condición posterior que desea probar e intente crear un invariante que lo ayude a llegar a la condición posterior paso a paso y que se pueda derivar del código del bucle.

Answer 3

No estoy seguro de si esto va a responder a su pregunta, pero por si acaso lo hace:

• un "lazo invariante" informalmente es una declaración de que sigue siendo cierto antes y después de una iteración de una lazo. Básicamente define la restricción de consistencia del programa con respecto a ese bucle.
• No sé lo suficiente acerca de Hoare Logic para decirle exactamente cómo un bucle invariante sería 'calculado', pero sospecho que tal cosa dependería del idioma del código que se analiza más que en el lenguaje de prueba formal en sí mismo . ¿Tiene una descripción algorítmica formal con la que está trabajando? Podría ser capaz de ir más allá con un poco más de fondo.
• Un invariante de bucle útil describiría algo específico sobre el estado de una aplicación. Por ejemplo, si estuviera escribiendo Clasificación de inserción, una invariante de bucle útil para el bucle de movimiento del elemento principal establecería esencialmente que la (sub) lista contiene la misma colección de objetos antes y después de la ejecución del bucle, y tal vez que los elementos que estaban previamente en orden ordenado permanecen en orden ordenado.