Cuando se utilizan aspectos formales para crear algún código, ¿existe un método genérico para determinar un bucle invariante o será completamente diferente según el problema?¿Cuál es la mejor manera de determinar un bucle invariante?
Ya se ha señalado que un mismo bucle puede tener varias invariantes, y que la calculabilidad está en su contra. No significa que no puedas intentarlo.
usted es, de hecho, buscando una inductiva invariante: la palabra invariante también puede ser utilizado para una propiedad que es cierto en cada iteración, pero para los que no es lo suficiente como para saber que se mantenga en una iteración a deduce que se mantiene en el siguiente. Si I es un invariante inductivo, entonces cualquier consecuencia de I es un invariante, pero puede que no sea un inductor inductivo.
Probablemente esté tratando de obtener una invariante inductiva para probar cierta propiedad (condición posterior) del ciclo en algunas circunstancias definidas (condiciones previas).
Hay dos heurísticas que funcionan bastante bien:
inicio con lo que tienes (precondiciones), y debilitar hasta que tenga un invariante inductivo. Para obtener una intuición sobre cómo debilitar, aplique una o varias iteraciones de bucle hacia adelante y vea qué deja de ser cierto en la fórmula que tiene.
comienza con lo que quieras (post-condiciones) y se fortalece hasta que tengas una invariante inductiva. Para obtener la intuición de cómo fortalecer, aplique una o varias iteraciones de bucle al revés y vea qué se debe agregar para que se pueda deducir la condición posterior.
Si desea que el equipo para ayudarle en su práctica, puedo recomendar el plug-in Jessie verificación deductiva de los programas en C de Frama-C. Hay otros, especialmente para las anotaciones Java y JML, pero estoy menos familiarizado con ellos. Probar las invariantes que piensas es mucho más rápido que hacer ejercicio si funcionan en papel. Debo señalar que la verificación de que una propiedad es una invariante inductiva también es indecidible, pero los modernos demostradores automáticos funcionan muy bien en muchos ejemplos simples. Si decide seguir esa ruta, obtenga tantos como pueda de la lista: Alt-ergo, Simplificar, Z3.
Con el delantal de biblioteca opcional (y un poco difícil de instalar), Jessie también puede infer some simple invariants automatically.
No creo que sea fácil de automatizar. Desde wiki:
Debido a la similitud fundamental de bucles y programas recursivos, probar la corrección parcial de bucles con invariantes es muy similar a probar la corrección de programas recursivos mediante inducción. De hecho, el bucle invariante es a menudo la propiedad inductiva que uno tiene que probar de un programa recursivo que es equivalente a un bucle dado.
Gracias, no quiero automatizarlo, es solo para ejercicios de lápiz y papel donde necesito encontrar invariantes de bucle. Supongo que solo requiere práctica. – filinep
En realidad, es trivial generar invariantes de bucle. true es bueno, por ejemplo. Cumple con todas las tres propiedades desea:
Pero lo que está buscando es probablemente el más fuerte loop invariant. Sin embargo, encontrar el invariante de bucle más fuerte es a veces incluso una tarea indecidible. Consulte el artículo Insuficiencia de invariantes de bucle computables.
"Verdadero" es débil. Creo que te refieres a "buscas la invariante de bucle * más fuerte *". Su respuesta ha arrojado un buen punto, pero yo diría que, por lo general, uno necesita "cualquier invariante inductivo lo suficientemente fuerte como para probar la propiedad que uno tiene en mente". El invariante de bucle más fuerte puede no existir (si hay una infinidad de variables, agregar "y x '= x" para una nueva x a un invariante crea un invariante más fuerte) y puede ser difícil de manejar. –
En cuanto a "más débil", tienes razón, por supuesto. ¡Lo tengo mezclado! (Pensé en ello como "verdadero es débil ya que no implica nada"). Respuesta actualizada Sin embargo, su segundo punto me parece ligeramente artificial. ¿Estás diciendo que no existe porque tomaría un espacio infinito anotarlo? – aioobe
Bueno, en la mayoría de las lógicas, una fórmula es un conjunto finito de símbolos, y supongo que algunos metatelogramas no serían ciertos si permitieras ensamblajes infinitos, incluso limitándote a ensamblajes regulares que pueden describirse finitamente. Así que hay que tener cuidado. Dejando a un lado este pequeño detalle (en ACSL se puede establecer la invariancia de variables infinitas en una cláusula finita, por ejemplo), mi punto fue que el invariante más fuerte puede ser mucho más complejo de lo necesario. –
Hay una serie de heurísticas para encontrar invariantes de bucle. Un buen libro sobre esto es "Programación en la década de 1990" de Ed Cohen. Se trata de cómo encontrar una buena invariante manipulando la poscondición a mano. Algunos ejemplos son: reemplazar una constante por una variable, fortalecer invariante, ...
He escrito sobre la escritura de invariantes de bucle en mi blog, vea Verifying Loops Part 2. Las invariantes necesarias para probar un bucle correcto generalmente constan de 2 partes:
(2) es sencillo. Para derivar (1), comience con un predicado que exprese el estado deseado después de la terminación. Lo más probable es que contenga un 'forall' o 'exists' en algún rango de datos. Ahora cambie los límites de 'forall' o 'exists' para que (a) dependan de las variables modificadas por el bucle (por ejemplo, contadores de bucle), y (b) para que el invariante sea trivialmente verdadero cuando se ingrese el bucle por primera vez (generalmente haciendo el rango del 'forall' o 'exists' vacío).
Bueno, ahí está. La respuesta perfecta. +1 :) Sin embargo, ¿alguna vez has visto que Simplify resuelva una obligación en la que Alt-ergo o Z3 fallaron?:-) – aioobe
@aioobe En este artículo, a Simplify le está yendo bien, y en la figura 1 hay una obligación con la propiedad que usted solicita (tanto Alt-ergo como Z3 fallan). Todo depende del programa de destino, por supuesto :) http://www-lipn.univ-paris13.fr/~mayero/publis/Calculemus2010.pdf –
Aha, nice :-) primero que he visto :) – aioobe