Defensa Tesis Licenciatura Jonathan Tapicer

• Título: Especificación y verificación modular de consumo de memoria
• Directores: Diego Garbervetsky y Martín Rouaux
• Jurados: Juan Pablo Galeotti, Daniel Gorín
• Resumen:

Abordamos en este trabajo la problemática de la verificación modular del consumo de memoria en programas orientados a objetos. El enfoque propuesto consiste en permitir al usuario anotar el programa con contratos asociados al consumo de memoria del mismo y luego verificar su correctitud, obteniendo así un certificado del consumo máximo de memoria del programa.

Para representar el hecho de que la memoria es recolectada automáticamente por un garbage collector en los lenguajes orientados a objetos del estilo de Java y C#, utilizaremos un modelo simplificado de administración de memoria basado en scopes. Definimos la sintaxis y semántica de un lenguaje de anotaciones para escribir contratos modulares de consumo de memoria en el código. Este lenguaje es suficientemente expresivo para brindar información de tiempo de vida de los objetos y contempla mecanismos de ocultamiento de la información para mantener la modularidad.

Se diseñan y detallan un conjunto de técnicas de instrumentación y verificación de los contratos, que apoyadas en un verificador estático permiten desarrollar una solución capaz de verificar la correctitud de los contratos dados en las anotaciones definidas.

La verificación de los contratos requiere muchas veces de una capacidad de análisis aritmético complejo. Dadas las limitaciones en el módulo aritmético de las mayoría de los verificadores estáticos existentes, proponemos un conjunto de técnicas adicionales que permiten integrar herramientas externas al proceso de verificación, haciendo posible la verificación de contratos con requerimientos aritméticos complejos.

Realizamos una implementación de prueba de concepto de las anotaciones y técnicas desarrolladas en el trabajo para la plataforma .NET utilizando las capacidades de verificación de la herramienta Code Contracts.