Contractor.NET: Inferring typestate properties to enrich code contracts

In this work we present Contractor.NET, a Visual Studio extension that supports the construction of contract specifications with typestate information which can be used for verification of client code. Contractor.NET uses and extends Code Contracts to provide stronger contract specifications. It fea...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Braberman, Víctor Adrián, de Caso, Guido, Garbervetsky, Diego
Publicado: 2011
Materias:
Contract strengthening
Enabledness abstractions
Typestate inference
Client code
Contract specifications
Finite state
Level of abstraction
MicroSoft
Software artifacts
Source codes
Two-step process
Typestate
Visual studios
Abstracting
Windows operating system
Specifications
Acceso en línea:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_02705257_v_n_p44_Zoppi
http://hdl.handle.net/20.500.12110/paper_02705257_v_n_p44_Zoppi
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id paper:paper_02705257_v_n_p44_Zoppi
record_format dspace
spelling paper:paper_02705257_v_n_p44_Zoppi2023-06-08T15:24:40Z Contractor.NET: Inferring typestate properties to enrich code contracts Braberman, Víctor Adrián de Caso, Guido Garbervetsky, Diego Contract strengthening Enabledness abstractions Typestate inference Client code Contract specifications Enabledness abstractions Finite state Level of abstraction MicroSoft Software artifacts Source codes Two-step process Typestate Visual studios Abstracting Windows operating system Specifications In this work we present Contractor.NET, a Visual Studio extension that supports the construction of contract specifications with typestate information which can be used for verification of client code. Contractor.NET uses and extends Code Contracts to provide stronger contract specifications. It features a two step process. First, a class source code is analyzed to extract a finite state behavior model (in the form of a typestate) that is amenable to human-in-theloop validation and refinement. The second step is to augment the original contract specification for the input class with the inferred typestate information, therefore enabling the verification of client code. The inferred typestates are enabledness preserving: a level of abstraction that has been successfully used to validate software artifacts, assisting in the detection of a number of concerns in various case studies including specifications of Microsoft Server protocols. Copyright 2011 ACM. Fil:Braberman, V. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:De Caso, G. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Garbervetsky, D. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. 2011 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_02705257_v_n_p44_Zoppi http://hdl.handle.net/20.500.12110/paper_02705257_v_n_p44_Zoppi
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic Contract strengthening
Enabledness abstractions
Typestate inference
Client code
Contract specifications
Enabledness abstractions
Finite state
Level of abstraction
MicroSoft
Software artifacts
Source codes
Two-step process
Typestate
Visual studios
Abstracting
Windows operating system
Specifications
spellingShingle Contract strengthening
Enabledness abstractions
Typestate inference
Client code
Contract specifications
Enabledness abstractions
Finite state
Level of abstraction
MicroSoft
Software artifacts
Source codes
Two-step process
Typestate
Visual studios
Abstracting
Windows operating system
Specifications
Braberman, Víctor Adrián
de Caso, Guido
Garbervetsky, Diego
Contractor.NET: Inferring typestate properties to enrich code contracts
topic_facet Contract strengthening
Enabledness abstractions
Typestate inference
Client code
Contract specifications
Enabledness abstractions
Finite state
Level of abstraction
MicroSoft
Software artifacts
Source codes
Two-step process
Typestate
Visual studios
Abstracting
Windows operating system
Specifications
description In this work we present Contractor.NET, a Visual Studio extension that supports the construction of contract specifications with typestate information which can be used for verification of client code. Contractor.NET uses and extends Code Contracts to provide stronger contract specifications. It features a two step process. First, a class source code is analyzed to extract a finite state behavior model (in the form of a typestate) that is amenable to human-in-theloop validation and refinement. The second step is to augment the original contract specification for the input class with the inferred typestate information, therefore enabling the verification of client code. The inferred typestates are enabledness preserving: a level of abstraction that has been successfully used to validate software artifacts, assisting in the detection of a number of concerns in various case studies including specifications of Microsoft Server protocols. Copyright 2011 ACM.
author Braberman, Víctor Adrián
de Caso, Guido
Garbervetsky, Diego
author_facet Braberman, Víctor Adrián
de Caso, Guido
Garbervetsky, Diego
author_sort Braberman, Víctor Adrián
title Contractor.NET: Inferring typestate properties to enrich code contracts
title_short Contractor.NET: Inferring typestate properties to enrich code contracts
title_full Contractor.NET: Inferring typestate properties to enrich code contracts
title_fullStr Contractor.NET: Inferring typestate properties to enrich code contracts
title_full_unstemmed Contractor.NET: Inferring typestate properties to enrich code contracts
title_sort contractor.net: inferring typestate properties to enrich code contracts
publishDate 2011
url https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_02705257_v_n_p44_Zoppi
http://hdl.handle.net/20.500.12110/paper_02705257_v_n_p44_Zoppi
work_keys_str_mv AT brabermanvictoradrian contractornetinferringtypestatepropertiestoenrichcodecontracts
AT decasoguido contractornetinferringtypestatepropertiestoenrichcodecontracts
AT garbervetskydiego contractornetinferringtypestatepropertiestoenrichcodecontracts
_version_ 1768546627542319104

Ejemplares similares