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: | |
---|---|
Formato: | Tesis de Grado |
Lenguaje: | Español |
Publicado: |
Dici
|
Acceso en línea: | https://hdl.handle.net/20.500.12110/seminario_nCOM000458_Zoppi |
Aporte de: |
id |
todo:seminario_nCOM000458_Zoppi |
---|---|
record_format |
dspace |
spelling |
todo:seminario_nCOM000458_Zoppi2023-10-03T16:48:38Z Enriqueciendo Code Contracts con Typestates Zoppi, Edgardo Julio 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. Fil: Zoppi, Edgardo Julio. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Diciembre 2012 Tesis de Grado PDF Español info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar https://hdl.handle.net/20.500.12110/seminario_nCOM000458_Zoppi |
institution |
Universidad de Buenos Aires |
institution_str |
I-28 |
repository_str |
R-134 |
collection |
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) |
language |
Español |
orig_language_str_mv |
Español |
description |
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. |
format |
Tesis de Grado |
author |
Zoppi, Edgardo Julio |
spellingShingle |
Zoppi, Edgardo Julio Enriqueciendo Code Contracts con Typestates |
author_facet |
Zoppi, Edgardo Julio |
author_sort |
Zoppi, Edgardo Julio |
title |
Enriqueciendo Code Contracts con Typestates |
title_short |
Enriqueciendo Code Contracts con Typestates |
title_full |
Enriqueciendo Code Contracts con Typestates |
title_fullStr |
Enriqueciendo Code Contracts con Typestates |
title_full_unstemmed |
Enriqueciendo Code Contracts con Typestates |
title_sort |
enriqueciendo code contracts con typestates |
publishDate |
Dici |
url |
https://hdl.handle.net/20.500.12110/seminario_nCOM000458_Zoppi |
work_keys_str_mv |
AT zoppiedgardojulio enriqueciendocodecontractscontypestates |
_version_ |
1782030490951221248 |