|
Descripción
|
|
|---|---|
| Detectar comportamientos incorrectos en los programas es una parte importante en el ciclo de desarrollo de software. Es una tarea compleja y tediosa, especialmente en el contexto de los lenguajes dinámicos. Se han propuesto numerosas técnicas que ayudan en el proceso, entre las cuales nos hemos centrado en el uso de construcciones a nivel de lenguaje para describir el comportamiento esperado del programa, y en las herramientas necesarias para comparar el comportamiento real del programa en contraposición con el esperado, como, por ejemplo, analizadores/verificadores estáticos de código y entornos de verificación en tiempo de ejecución. En la práctica, sin embargo, el alto coste durante la ejecución hace que el uso de estas herramientas sea poco viable, especialmente para propiedades complejas. Esto reduce el interés en hacer comprobaciones en tiempo de ejecución desde el punto de vista de los programadores y programadoras, quienes esporádicamente permitirán comprobaciones de condiciones muy sencillas pero tenderán a desactivarlas para propiedades complejas. Algunos trabajos optan por limitar la expresividad del lenguaje de aserciones para reducir este coste. Con esta motivación, el objetivo de esta tésis es doble: - primero, pretendemos mejorar la expresividad del lenguaje de aserciones para reflejar todas las características relacionadas con el lenguaje de programación, incluyendo, por ejemplo, construcciones de orden superior, haciéndolo de forma que el/la programador/ a pueda escribir especificaciones sin necesidad de aprender o programar para ello; - al mismo tiempo, nuestra meta es comprobar de forma eficiente dichas especificaciones, reduciendo el coste asociado en tiempo de ejecución en la medida de lo posible y sin comprometer las garantías de seguridad que proporcionan dichas comprobaciones. Esta tésis presenta varias mejoras para la comprobación de especificaciones en tiempo de ejecución entre las que se encuentran: - un mecanismo discreto de memorización de resultados intermedios de comprobación, de forma que pueden ser reutilizados en el proceso de comprobación en lugar de recalcularlos; - un técnica que combina comprobación en tiempo de compilación y en tiempo de ejecución, que usa las propiedades de esta última como información adicional en tiempo de compilación, lo que implica que más propiedades se puedan comprobar estáticamente, aligerando el trabajo en tiempo de ejecución; - y otra técnica para mejorar la inferencia de estructuras durante el análisis estático de programas, que aprovecha las reglas de visibilidad de términos del entorno modular subyacente, lo que permite simplificar las comprobaciones de propiedades del programa consiguiendo un sobrecoste constante en casos relevantes. Finalmente, para atacar el problema de la expresividad limitada de los lenguajes de especificaciones, esta tésis se enfoca en el caso concreto de aportar especificaciones detalladas para rutinas de orden superior. Las técnicas y herramientas estudiadas en esta tésis se presentan, por concreción, en el entorno de comprobación en tiempo de ejecución Ciao. No obstante, los resultados son generales e independientes del sistema, y creemos que pueden trasladarse de forma sencilla a otros lenguajes de programación declarativos. Además, dados los avances en verificación en gran parte de los lenguajes de programación, incluyendo los imperativos, mediante la traducción a cláusulas de Horn y probando propiedades a este nivel, y el hecho de que este enfoque está totalmente soportado en el sistema Ciao, argumentamos que nuestros resultados se pueden adaptar fácilmente a un espectro mucho mas amplio de lenguajes. | |
|
Internacional
|
No |
|
ISBN
|
|
|
Tipo de Tesis
|
Doctoral |
|
Calificación
|
Sobresaliente cum laude |
|
Fecha
|
23/05/2018 |