Ya se ha señalado que un mismo bucle puede tener varios invariantes, y que la Calculabilidad está en su contra. No significa que no puedas intentarlo.
De hecho, está buscando una invariante inductiva : la palabra invariante también puede usarse para una propiedad que es verdadera en cada iteración pero para la cual no es suficiente saber que se mantiene en una iteración para deducir que se mantiene en la siguiente. Si I es una invariante inductiva, entonces cualquier consecuencia de I es una invariante, pero puede no ser una invariante inductiva.
Probablemente esté tratando de obtener una invariante inductiva para probar una determinada propiedad (condición posterior) del bucle en algunas circunstancias definidas (condiciones previas).
- ¿Qué matemática se requiere para comenzar a aprender sobre el análisis de riesgos?
- ¿Por qué hacemos análisis funcionales?
- ¿Cómo factorizarías (1 + 2x - 6x ^ 3 - 9x ^ 4)?
- ¿Cuál es la próxima prueba experimental sobresaliente de una teoría existente?
- ¿Cuáles son las unidades de dígitos de 2017 ^ 2017?
Hay dos heurísticas que funcionan bastante bien:
- comience con lo que tiene (condiciones previas) y debilítese hasta que tenga una invariante inductiva. Para tener una intuición sobre cómo debilitarse, aplique una o varias iteraciones de bucle hacia adelante y vea qué deja de ser cierto en la fórmula que tiene.
- Comience con lo que desea (post-condiciones) y fortalezca hasta que tenga una invariante inductiva. Para obtener la intuición de cómo fortalecer, aplique una o varias iteraciones de bucle hacia atrás y vea qué se debe agregar para que se pueda deducir la condición posterior.
Si desea que la computadora lo ayude en su práctica, puedo recomendar el complemento de verificación deductiva Jessie para los programas C de Frama-C. Hay otros, especialmente para las anotaciones Java y JML, pero estoy menos familiarizado con ellas. Probar los invariantes que piensas es mucho más rápido que hacer ejercicio si funcionan en papel. Debo señalar que verificar que una propiedad es una invariante inductiva también es indecidible, pero los comprobadores automáticos modernos funcionan muy bien en muchos ejemplos simples. Si decide seguir esa ruta, obtenga tantos como pueda de la lista: Alt-ergo, Simplificar, Z3.
s / ource /: ¿Cuál es la mejor manera de determinar un bucle invariante?
