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...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: Zoppi, Edgardo Julio
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