Compresión automática de contratos software

Abstract

[ES] En Ingeniería de Software, el concepto de contrato está relacionado con una especificación del comportamiento de los programas utilizando descripciones que típicamente incluyen precondiciones y postcondiciones. El estado del arte actual permite generar automáticamente contratos a partir del código fuente que pueden ser usados como entrada para analizadores cada vez más potentes. Sin embargo, los contratos generados automáticamente pueden contener axiomas redundantes o demasiado específicos. El objetivo de este proyecto es desarrollar una aplicación que permite sintetizar, simplificar y comparar dichos contratos en varias formas: 1) identificando y eliminando axiomas redundantes; 2) generalizando un conjunto de axiomas particulares a axiomas más generales bajo subsumción de restricciones; y 3) analizando la evolución del software mediante comparación de contratos.

[EN] Software contracts provide formal specification for the terms of the service that software components can provide. Contracts on software are essentially written by using program preconditions and postconditions that formalize the mutual obligations and benefits of the software units or routines. The current state of the art allows contracts to be automatically inferred from the source code so that can be used as input for increasingly powerful analyzers. However, automatically generated contracts can contain some redundant or overly specific components. The goal of this project is to develop a software application that allows contracts to be synthesized, simplified, and compared in several ways: 1) by identifying and removing redundant axioms; and 2) by generalizing a set of axioms into more general axioms under constraint subsumption; and 3) comparing contracts to analyze the software evolution.