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...
Guardado en:
| Autores principales: | , , , , |
|---|---|
| Formato: | CONF |
| Materias: | |
| Acceso en línea: | http://hdl.handle.net/20.500.12110/paper_02705257_v_n_p44_Zoppi |
| Aporte de: |
| id |
todo:paper_02705257_v_n_p44_Zoppi |
|---|---|
| record_format |
dspace |
| spelling |
todo:paper_02705257_v_n_p44_Zoppi2023-10-03T15:14:31Z Contractor.NET: Inferring typestate properties to enrich code contracts Zoppi, E. Braberman, V. De Caso, G. Garbervetsky, D. Uchitel, S. 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. CONF info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar 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 Zoppi, E. Braberman, V. De Caso, G. Garbervetsky, D. Uchitel, S. 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. |
| format |
CONF |
| author |
Zoppi, E. Braberman, V. De Caso, G. Garbervetsky, D. Uchitel, S. |
| author_facet |
Zoppi, E. Braberman, V. De Caso, G. Garbervetsky, D. Uchitel, S. |
| author_sort |
Zoppi, E. |
| 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 |
| url |
http://hdl.handle.net/20.500.12110/paper_02705257_v_n_p44_Zoppi |
| work_keys_str_mv |
AT zoppie contractornetinferringtypestatepropertiestoenrichcodecontracts AT brabermanv contractornetinferringtypestatepropertiestoenrichcodecontracts AT decasog contractornetinferringtypestatepropertiestoenrichcodecontracts AT garbervetskyd contractornetinferringtypestatepropertiestoenrichcodecontracts AT uchitels contractornetinferringtypestatepropertiestoenrichcodecontracts |
| _version_ |
1807317633082589184 |