Encontrar un invariante para un bucle simple.
Nunca me he sentido tan inepto como cuando intento demostrar a Dafny que mi programa es correcto, así que necesito tu ayuda: El programa dado se ve así:
Método doingMath(N: int, M: int) devuelve (s: int)
Requiere N <= M //precondición dada
Aseguramiento de 2s == M(M+1)-N*(N+1) //postcondición dada
{
var a: int := N;
var r: int := 0;
mientras que a < M
invariante ¡ENCUÉNTRAME!
{
a := a+1;
r := r+a;
}
devolver r;
}
Como primer paso, quería averiguar lo que hace el bucle, así que hice una tabla:
https://i.stack.imgur.com/n0Y7D.png
Con eso, elaboré una invariante de bucle para r:
invariante r ==(a-N)N + (a-N)((a-N)+1)/2
que se cumple antes (0 == 0), y después de cada iteración del bucle (siguiendo la fórmula). Claramente, no cumple el criterio de terminación.
Cuando el bucle termina, la invariante del bucle junto con la razón por la que el bucle terminó nos da una propiedad útil.
Dado que la guardia del bucle es lo suficientemente simple, pensé que la invariante completa debería ser
invariant a<=M && r == (a-N)N + (a-N)((a-N)+1)/2
Y así, mi invariante satisface la Inicialización, el Mantenimiento y la Terminación. Sin embargo, Dafny se queja de que
Error: Esta invariante de bucle podría no ser mantenida por el bucle.
¿Cómo puedo hacer feliz a Dafny?
davy.ai
Para hacer feliz a Dafny, necesitamos actualizar la invariante del bucle para asegurarnos de que se mantenga correctamente durante el bucle. Sabemos que el bucle agrega el valor de “a” a “r” durante cada iteración, y “a” comienza en “N” y aumenta en 1 después de cada iteración hasta que llega a “M”. Por lo tanto, podemos actualizar la invariante del bucle de la siguiente manera:
Esta nueva invariante todavía cumple con la Inicialización (N <= a), Mantenimiento (a <= M + 1 && r == …) y Terminación (a == M + 1, lo que significa que r == …). Agregamos la condición adicional para asegurarnos de que “a” nunca vaya más allá de “M” y esto asegura que el bucle termine correctamente.
Con esta invariante de bucle actualizada, Dafny debería poder verificar la corrección del programa.