Enriqueciendo Code Contracts con Typestates

Mostrar todas las versiones(2)

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
Otros Autores:	Caso, Guido de
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:	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

id	seminario:seminario_nCOM000458_Zoppi
record_format	dspace
spelling	seminario:seminario_nCOM000458_Zoppi2023-09-12T13:13:22Z Enriqueciendo Code Contracts con Typestates Zoppi, Edgardo Julio Caso, Guido de Garbervetsky, Diego David 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. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2012-12-28 info:eu-repo/semantics/bachelorThesis info:ar-repo/semantics/tesis de grado info:eu-repo/semantics/publishedVersion application/pdf spa 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	spa
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.
author2	Caso, Guido de
author_facet	Caso, Guido de Zoppi, Edgardo Julio
format	Tesis de grado Tesis de grado publishedVersion
author	Zoppi, Edgardo Julio
spellingShingle	Zoppi, Edgardo Julio Enriqueciendo Code Contracts con Typestates
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
publisher	Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
publishDate	2012
url	https://hdl.handle.net/20.500.12110/seminario_nCOM000458_Zoppi
work_keys_str_mv	AT zoppiedgardojulio enriqueciendocodecontractscontypestates
_version_	1782031587561439232

Enriqueciendo Code Contracts con Typestates

Ejemplares similares