Verificación de algoritmos de vuelta atrás en Dafny

Abstract

La verificación formal es una técnica que permite demostrar, mediante métodos matemáticos, que un programa cumple su especificación (el comportamiento esperado del programa). A diferencia de las pruebas tradicionales, no se basa en casos de prueba concretos, sino en razonamientos lógicos que garantizan la corrección del código en todos los casos posibles. En este trabajo desarrollaremos una metodología para especificar y verificar en Dafny algoritmos de vuelta atrás. Dicha metodología se aplica a dos ejemplos representativos de los problemas resueltos mediante este método algorítmico. En este trabajo hemos usado la herramienta Dafny, un lenguaje de programación diseñado para la especificación formal y la verificación asistida de programas. Se presentarán los elementos esenciales de la metodología utilizando como ejemplo el problema de la mochila. En dicho problema el espacio de búsqueda está estructurado como un árbol binario, lo que se traduce en invocar recursivamente al propio algoritmo dos veces a lo sumo (una cantidad fija). A continuación, extenderemos la metodología para especificar y verificar problemas en los que el espacio de búsqueda está estructurado como un árbol n-ario, lo cual implica un bucle de invocaciones recursivas donde el número de iteraciones depende de una de las dimensiones del problema. Concretamente, verificaremos el problema de asignar tareas a funcionarios. Completaremos la metodología introduciendo podas de optimalidad para reducir el espacio de búsqueda y proporcionaremos varias podas en ambos ejemplos de aplicación. Finalmente, se proporcionarán conclusiones y posibles líneas del trabajo futuro.