Enriqueciendo Code Contracts con Typestates
Por lo general un componente de software tiene requerimientos que no son para nada triviales cuando se trata del orden en que sus métodos o procedimientos pueden ser ejecutados. Esta situación es común, por ejemplo, en el caso de APIs que implementan protocolos. Este trabajo trata de ayudar en el pr...
Guardado en:
| Autor principal: | |
|---|---|
| Otros Autores: | |
| Formato: | Tesis de grado publishedVersion |
| Lenguaje: | Español |
| Publicado: |
Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
2012
|
| Acceso en línea: | https://hdl.handle.net/20.500.12110/seminario_nCOM000458_Zoppi |
| Aporte de: |
| Sumario: | Por lo general un componente de software tiene requerimientos que no son para nada triviales cuando se trata del orden en que sus métodos o procedimientos pueden ser ejecutados. Esta situación es común, por ejemplo, en el caso de APIs que implementan protocolos. Este trabajo trata de ayudar en el problema de validar si una implementación particular cumple con el comportamiento esperado en los casos en que su descripción es informal, parcial o directamente inexistente. Con esto en mente,presentamos Contractor.Net, una herramienta que permite construir especificaciones por contratos con información de typestate que puede ser utilizada para verificar código cliente. Contractor.Net usa y extiende Code Contracts para proveerespecicaciones por contratos más robustas. El proceso se realiza en dos etapas. Primero, el código fuente de una clase es analizado de forma estática para extraer un modelo abstracto finito de comportamiento (en la forma de typestate) adecuado para su validación y refinamiento por parte del programador. La segunda etapa consiste en aumentar la especificación por contratos original de la clase en cuestión con la información de typestate inferida en la etapa anterior, con el objetivo de proveer más datos para la verificación del código cliente. Los typestates inferidos cumplen con la propiedad enabledness preserving, un nivel de abstracción que mostró resultados positivos al momento de validar el modelo, ayudando a la detección de errores, ajustes en los requerimientos y la generación de documentación más completa y detallada. |
|---|