Artículo
Abstract:
We are interested in object-oriented programming methodologies that enable static verification of object-invariants. Reasoning soundly and effectively about the consistency of objects is still one of the main stumbling blocks to pushing object-oriented program verification into the mainstream. More precisely, any sound methodology must be able to guarantee that the invariant of the receiver object holds at all method call sites. Establishing this proof obligation is tedious, and instead programmers would like to reason informally as follows: methods should be able to assume that the object invariant holds on entry, as long as all constructors establish it, and all methods guarantee that the receiver invariant holds on exit. This reasoning is only correct under certain conditions. In this paper we present sufficient conditions that make reasoning as above sound and show how these conditions can be checked separately, allowing us to divide the verification problem into two well-defined parts: 1) reasoning about object consistency of the receiver within a single method, and 2) reasoning about the absence of inconsistent re-entrant calls. In particular, when reasoning about the object consistency of the receiver within a method, our approach does not require proving invariants on other objects whose methods are called. We present a novel whole program analysis to determine the absence of inconsistent re-entrant calls. It warns developers when re-entrant calls are made on objects whose invariants may not hold. The analysis augments a points-to analysis to compute potential call chains in order to detect re-entrant calls.
Registro:
| Documento: | Artículo |
| Título: | A static analysis to detect re-entrancy in object oriented programs |
| Autor: | Fähndrich, M.; Garbervetsky, D.; Schulte, W. |
| Filiación: | Microsoft Research, Redmond, WA, United States Departamento de Computación, FCEyN, UBA, Argentina |
| Año: | 2008 |
| Volumen: | 7 |
| Número: | 5 |
| Página de inicio: | 5 |
| Página de fin: | 23 |
| DOI: | http://dx.doi.org/10.5381/jot.2008.7.5.a1 |
| Título revista: | Journal of Object Technology |
| Título revista abreviado: | J. Object Technol. |
| ISSN: | 16601769 |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_16601769_v7_n5_p5_Fahndrich |
Referencias:
- Ball, T., Lahiri, S.K., Musuvathi, M., Zap: Automated theorem proving for software analysis (2005) Proceedings of the 12th International Conference on Logic for Programming, Aritificial Intelligence and Reasoning (LPAR '05), , October
- Barnett, M., DeLine, R., Fähndrich, M., Rustan, K., Leino, M., Schulte, W., Verification of object-oriented programs with invariants (2004) Journal of Object Technology, 3 (6), pp. 27-56
- Mike Barnett, Robert DeLine, Bart Jacobs, Bor-Yuh Evan Chang, and K. Rustan M. Leino. Boogie: A modular reusable verifier for object-oriented programs. In Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever, editors, FMCO 2005, 4111 of LNCS, pages 364-387. Springer, September 2006; Barnett, M., Fändrich, M., Garbervetsky, D., Logozzo, F., Annotations for (more) precise points-to analysis (2007) IWACO 2007: 2nd International Workshop on Aliasing, Confinement and Ownership in object-oriented programming, pp. 11-18. , Berlin, Germany, July
- Dave, G., Clarke, J., Potter, M., Noble, J., Ownership types for flexible alias protection (1998) OOPSLA '98, volume 33:10 of SIGPLANNotices, pp. 48-64. , ACM, October
- Detlefs, D., Nelson, G., Saxe, J.B., Simplify: A theorem prover for program checking (2005) Journal of the ACM, 52 (3), pp. 365-473. , May
- (2006) ECMA-335, Common Language Infrastructure (CLI), , http://www.ecma-international.org/publications/standards-/Ecma-335.htm
- Flanagan, C., Rustan, K., Leino, M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R., Extended static checking for java (2002) PLDI '02: Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, pp. 234-245. , New York, NY, USA, ACM Press
- Lam, P., Kuncak, V., Rinard, M., Generalized typestate checking using set interfaces and pluggable analyses (2004) SIGPLAN Not, 39 (3), pp. 46-55
- Meyer, B., Object-oriented Software Construction (1988) Series in Computer Science, , Prentice-Hall International, New York
- David A. Naumann and Mike Barnett. Towards imperative modules: Reasoning about invariants and sharing of mutable state. Theor. Comput. Sci., 365(1):143-168, 2006.f; Salcianu, A., Rinard, M., Purity and side effect analysis forjava programs (2005) Proceedings of the 6th International Conference on Verification, Model Checking and Abstract Interpretation, , January
Citas:
---------- APA ----------
Fähndrich, M., Garbervetsky, D. & Schulte, W. (2008) . A static analysis to detect re-entrancy in object oriented programs. Journal of Object Technology, 7(5), 5-23.http://dx.doi.org/10.5381/jot.2008.7.5.a1
---------- CHICAGO ----------
Fähndrich, M., Garbervetsky, D., Schulte, W. "A static analysis to detect re-entrancy in object oriented programs" . Journal of Object Technology 7, no. 5 (2008) : 5-23.http://dx.doi.org/10.5381/jot.2008.7.5.a1
---------- MLA ----------
Fähndrich, M., Garbervetsky, D., Schulte, W. "A static analysis to detect re-entrancy in object oriented programs" . Journal of Object Technology, vol. 7, no. 5, 2008, pp. 5-23.http://dx.doi.org/10.5381/jot.2008.7.5.a1
---------- VANCOUVER ----------
Fähndrich, M., Garbervetsky, D., Schulte, W. A static analysis to detect re-entrancy in object oriented programs. J. Object Technol. 2008;7(5):5-23.http://dx.doi.org/10.5381/jot.2008.7.5.a1
