Especificación de Contratos de Software con JML y Eiffel

En el presente trabajo se introduce el enfoque de diseño por contratos que se basa en los métodos formales para el diseño e implementación de aplicaciones y componentes. Se realiza un análisis de dos lenguajes de especificación formal, JML y Eiffel, que siguen el paradigma de diseño por contrato. JML permite realizar la especificación de productos de software desarrollados en Java y Eiffel es un lenguaje de programación pionero en introducir la noción de diseño por contratos. Se realiza un estudio de las herramientas vinculadas al JML, que permiten interpretar y ejecutar las especificaciones realizadas en dicho lenguaje. Se propone una nueva caracterización a partir del análisis de dos categorizaciones de herramientas, propuestas en otros trabajos. En el estudio de los dos lenguajes de especificación formal se realizan ejercicios prácticos, en particular se propuso la implementación y especificación de una Lista dinámica, la cual involucra la manipulacion de punteros, comportamiento que nos pareció interesante de especificar en ambos lenguajes. Para la resolución del ejercicio en el JML se utilizaron algunas de las herramientas estudiadas. Los principales factores utilizados para elegir las mismas fueron de acuerdo a la documentación disponible y continuidad de versiones.