Traducción de contratos software a un lenguaje de especificación estándar

Abstract

[ES] El diseño por contrato es una metodología de programación que requiere que el programador proporcione, en tiempo de diseño, contratos (o anotaciones) que definen el comportamiento del código. Los contratos tienen numerosos usos en este contexto. Por ejemplo, permiten la generación automática de documentación, potencian el proceso de prueba y son el soporte natural para las técnicas de verificación automática.

Durante el mantenimiento del código, los contratos quedan fácilmente obsoletos y recientemente están cobrando gran interés las técnicas capaces de generar automáticamente dichos contratos. No obstante, una dificultad para la difusión de estas técnicas es la notación que utilizan para expresar los contratos son fórmulas lógicas con las que, pese a su simplicidad, no todos los desarrolladores están familiarizados..

El trabajo que se plantea en este proyecto es desarrollar un programa que traduzca las anotaciones escritas en la notación lógica a un formato de salida estándar en el que expresar contratos para el código C como ACSL (el equivalente para C del JML).

[EN] Design by contract is a programming methodology that requires the programmer to provide, at design time, contracts (or annotations) that define the behavior of the code. Contracts have numerous uses in this context. For example, they enable the automatic generation of documentation, enhance the testing process and are the natural support for automatic verification techniques. During code maintenance, contracts easily become obsolete and techniques capable of automatically generating such contracts have recently become of great interest. However, a difficulty for the diffusion of these techniques is the notation used to express the contracts are logical formulas with which, despite their simplicity, not all developers are familiar. The work involved in this project is to develop a program that translates annotations written in logic notation into a standard output format in which to express contracts for C code such as ACSL (the C equivalent of JML).