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:
| Autor principal: | |
|---|---|
| Otros Autores: | , , , |
| Formato: | Acta de conferencia Capítulo de libro |
| Lenguaje: | Inglés |
| Publicado: |
2011
|
| Acceso en línea: | Registro en Scopus DOI Handle Registro en la Biblioteca Digital |
| Aporte de: | Registro referencial: Solicitar el recurso aquí |
| LEADER | 04294caa a22006377a 4500 | ||
|---|---|---|---|
| 001 | PAPER-10467 | ||
| 003 | AR-BaUEN | ||
| 005 | 20230518204030.0 | ||
| 008 | 190411s2011 xx ||||fo|||| 10| 0 eng|d | ||
| 024 | 7 | |2 scopus |a 2-s2.0-79959859908 | |
| 040 | |a Scopus |b spa |c AR-BaUEN |d AR-BaUEN | ||
| 030 | |a PCSED | ||
| 100 | 1 | |a Zoppi, E. | |
| 245 | 1 | 0 | |a Contractor.NET: Inferring typestate properties to enrich code contracts |
| 260 | |c 2011 | ||
| 270 | 1 | 0 | |m Zoppi, E.; Departamento de Computación, FCEyN, UBA, Buenos Aires, Argentina; email: ezoppi@dc.uba.ar |
| 506 | |2 openaire |e Política editorial | ||
| 504 | |a Ball, T., Rajamani, S., The SLAM project: Debugging system software via static analysis (2002) POPL '02, pp. 1-3 | ||
| 504 | |a Bodden, E., Lam, P., Hendren, L., Finding programming errors earlier by evaluating runtime monitors ahead-of-time (2008) FSE '08, pp. 36-47 | ||
| 504 | |a De Caso, G., Braberman, V., Garbervetsky, D., Uchitel, S., Program abstractions for behaviour validation (2011) ICSE 2011, , to be published | ||
| 504 | |a DeLine, R., Fahndrich, M., Typestates for objects (2004) LNCS, pp. 465-490. , ECOOP'04 | ||
| 504 | |a Fähndrich, M., Barnett, M., Logozzo, F., Embedded contract languages (2010) SAC'10, pp. 2103-2110 | ||
| 504 | |a Henzinger, T.A., Jhala, R., Majumdar, R., Permissive interfaces (2005) FSE '05, pp. 31-40 | ||
| 504 | |a Kim, T., Bierhoff, K., Aldrich, J., Kang, S., Typestate protocol specification in JML (2009) SAVCBS '09, pp. 11-18. , ACMA4 - ACM SIGSOFT; IEEE CS | ||
| 520 | 3 | |a 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. |l eng | |
| 593 | |a Departamento de Computación, FCEyN, UBA, Buenos Aires, Argentina | ||
| 690 | 1 | 0 | |a CONTRACT STRENGTHENING |
| 690 | 1 | 0 | |a ENABLEDNESS ABSTRACTIONS |
| 690 | 1 | 0 | |a TYPESTATE INFERENCE |
| 690 | 1 | 0 | |a CLIENT CODE |
| 690 | 1 | 0 | |a CONTRACT SPECIFICATIONS |
| 690 | 1 | 0 | |a ENABLEDNESS ABSTRACTIONS |
| 690 | 1 | 0 | |a FINITE STATE |
| 690 | 1 | 0 | |a LEVEL OF ABSTRACTION |
| 690 | 1 | 0 | |a MICROSOFT |
| 690 | 1 | 0 | |a SOFTWARE ARTIFACTS |
| 690 | 1 | 0 | |a SOURCE CODES |
| 690 | 1 | 0 | |a TWO-STEP PROCESS |
| 690 | 1 | 0 | |a TYPESTATE |
| 690 | 1 | 0 | |a VISUAL STUDIOS |
| 690 | 1 | 0 | |a ABSTRACTING |
| 690 | 1 | 0 | |a WINDOWS OPERATING SYSTEM |
| 690 | 1 | 0 | |a SPECIFICATIONS |
| 700 | 1 | |a Braberman, V. | |
| 700 | 1 | |a De Caso, G. | |
| 700 | 1 | |a Garbervetsky, D. | |
| 700 | 1 | |a Uchitel, S. | |
| 711 | 2 | |c Waikiki, Honolulu, HI |d 28 May 2011 through 28 May 2011 |g Código de la conferencia: 85372 | |
| 773 | 0 | |d 2011 |h pp. 44-47 |p Proc Int Conf Software Eng |n Proceedings - International Conference on Software Engineering |x 02705257 |z 9781450305990 |t 1st Workshop on Developing Tools as Plug-ins, TOPI 2011, Co-located with ICSE 2011 | |
| 856 | 4 | 1 | |u https://www.scopus.com/inward/record.uri?eid=2-s2.0-79959859908&doi=10.1145%2f1984708.1984721&partnerID=40&md5=35cce7356b3eca5592da385276ef2c32 |y Registro en Scopus |
| 856 | 4 | 0 | |u https://doi.org/10.1145/1984708.1984721 |y DOI |
| 856 | 4 | 0 | |u https://hdl.handle.net/20.500.12110/paper_02705257_v_n_p44_Zoppi |y Handle |
| 856 | 4 | 0 | |u https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_02705257_v_n_p44_Zoppi |y Registro en la Biblioteca Digital |
| 961 | |a paper_02705257_v_n_p44_Zoppi |b paper |c PE | ||
| 962 | |a info:eu-repo/semantics/conferenceObject |a info:ar-repo/semantics/documento de conferencia |b info:eu-repo/semantics/publishedVersion | ||
| 999 | |c 71420 | ||