Termination analysis of programs with complex control-flow

Resumen

El problema de la terminación de un programa es fundamental en informática y ha sido objeto de estudio de numerosas investigaciones. La técnica mejor conocida, y más frecuentemente utilizada, para demostrar terminación es el uso de funciones de clasificación. Estas funciones relacionan los estados del programa con los elementos de un conjunto ordenado bien-fundado, tal que el valor desciende en estados consecutivos del programa. Como descender en un conjunto ordenado bien-fundado no puede hacerse de manera infinita se demuestra la terminación del programa. Además de demostrar terminación, algunas clases de funciones de clasificación sirven para determinar la cota de la longitud de la ejecución, útil en aplicaciones como el análisis de coste. A diferencia de la terminación de programas en general, que es indecidible, los problemas algorítmicos de detección y generación de funciones de clasificación pueden ser resueltos dadas ciertas elecciones de la representación del programa y la clase de funciones de clasificación. Para muchas clases estos problemas algorítmicos han sido completamente resueltos, y se provee de algoritmos eficientes, mientras que para otras aún permanecen abiertos. Esta tesis se aborda el problema de terminación para Sistemas de Transiciones con valores numéricos que son una representación de programas muy comúnmente utilizada en los análisis de programas, usando funciones de clasificación lineales. Los principales resultados son: (i) Las funciones de clasificación multi-fase se usan para demostrar la terminación de programas en los que la ejecución progresa por medio de un número de fases. En esta tesis se proporcionan nuevos conocimientos sobre estas funciones. Concretamente, (i.1) para el problema de decisión de la existencia de estas funciones, se progresa identificando las clases de bucles para los que estas funciones son suficientes, y así tener cotas en tiempo de ejecución lineales; y (i.2) el problema acotado de decisión que restringe la búsqueda de estas funciones a tuplas con d elementos, se obtiene un nuevo método de tiempo polinómico que puede proporcionar también pruebas para respuestas negativas ya que se relaciona este problema con el de encontrar conjuntos de recurrencia (usados para demostrar no terminación). Para obtener los resultados de ambos problemas, se introduce una nueva representación para los bucles que revela información difícil de ver en otras representaciones estándar. (ii) Desarrollar transformadores de programas para simplificar el flujo de control de un programa, es otra técnica utilizada para mejorar los resultados de los análisis. Varias de estas técnicas han sido sugeridas a medida para diferentes modelos de programación. En esta tesis, se sugiere el uso de Evaluación Parcial como transformador de programas de uso general. Usar evaluación parcial tiene la ventaja de que la validez de la transformación se obtiene de las propiedades generales del método. Se usa un algoritmo de evaluación parcial que incorpora abstracción basada en propiedades, y se ve cómo la correcta elección de propiedades permite demostrar terminación e inferir el coste de programas complicados que hasta ahora no podían ser tratados por las herramientas actuales. Se aporta iRankFinder, un analizador de terminación que implementa todas las técnicas desarrolladas en esta tesis. Así como, una evaluación experimental de iRankFinder que demuestra la utilidad de esas técnicas. Además, se provee con una implementación independiente del refinamiento propuesto que puede ser integrada fácilmente en programas ya existentes. Sin embargo, en lugar de construir una interfaz web hecha a medida para el uso de estas herramientas se aporta un conjunto de herramientas, llamado EasyInterface, que simplifica el proceso de construir interfaces de usuario para prototipos.