ABSTRACT
Objects often define usage protocols that clients must follow inorder for these objects to work properly. Aliasing makes itnotoriously difficult to check whether clients and implementations are compliant with such protocols. Accordingly, existing approaches either operate globally or severely restrict aliasing.
We have developed a sound modular protocol checking approach, based on typestates, that allows a great deal of flexibility in aliasing while guaranteeing the absence of protocol violations at runtime. The main technical contribution is a novel abstraction, access permissions, that combines typestate and object aliasing information. In our methodology, developers express their protocol design intent through annotations based on access permissions. Our checking approach then tracks permissions through method implementations. For each object reference the checker keeps track of the degree of possible aliasing and is appropriately conservativein reasoning about that reference. This helps developers account for object manipulations that may occur through aliases. The checking approach handles inheritance in a novel way, giving subclasses more flexibility in method overriding. Case studies on Java iterators and streams provide evidence that access permissions can model realistic protocols, and protocol checking based on access permissions can be used to reason precisely about the protocols that arise in practice.
- T. Ball and S. K. Rajamani. Automatically validating temporal safety properties of interfaces. In Proc. of the Eighth SPIN Workshop, pages 101--122, May 2001. Google ScholarDigital Library
- M. Barnett, R. DeLine, M. Fähndrich, K. R. M. Leino, and W. Schulte. Verification of object-oriented programs with invariants. Journal of Object Technology, 3(6):27--56, June 2004.Google ScholarCross Ref
- K. Bierhoff. Iterator specification with typestates. In 5th Int. Workshop on Specification and Verification of Component- Based Systems, pages 79--82. ACM Press, Nov. 2006. Google ScholarDigital Library
- K. Bierhoff and J. Aldrich. Lightweight object specification with typestates. In Joint European Software Engineering Conference and ACM Symposium on the Foundations of Software Engineering, pages 217--226. ACM Press, Sept. 2005. Google ScholarDigital Library
- K. Bierhoff and J. Aldrich. Modular typestate verification of aliased objects. Technical Report CMUISRI-07-105, Carnegie Mellon University, Mar. 2007. http://reports-archive.adm.cs.cmu.edu/anon/isri2007/CMUISRI-07-105.pdf.Google ScholarCross Ref
- J. Boyland. Checking interference with fractional permissions. In Int. Symposium on Static Analysis, pages 55--72. Springer, 2003.Google ScholarCross Ref
- J. T. Boyland and W. Retert. Connecting effects and uniqueness with adoption. In ACM Symposium on Principles of Programming Languages, pages 283--295, Jan. 2005. Google ScholarDigital Library
- S. Chaki, E. Clarke, A. Groce, S. Jha, and H. Veith. Modular verification of software components in C. In Int. Conference on Software Engineering, pages 385--395, May 2003. Google ScholarDigital Library
- W.-N. Chin, S.-C. Khoo, S. Qin, C. Popeea, and H. H. Nguyen. Verifying safety policies with size properties and alias controls. In Int. Conference on Software Engineering, pages 186--195, May 2005. Google ScholarDigital Library
- M. Degen, P. Thiemann, and S. Wehr. Tracking linear and affine resources with Java(X). In European Conference on Object-Oriented Programming. Springer, Aug. 2007. Google ScholarDigital Library
- R. DeLine and M. Fähndrich. Enforcing high-level protocols in low-level software. In ACM Conference on Programming Language Design and Implementation, pages 59--69, 2001. Google ScholarDigital Library
- R. DeLine and M. Fähndrich. Typestates for objects. In European Conference on Object-Oriented Programming, pages 465--490. Springer, 2004.Google ScholarCross Ref
- M. Fähndrich and R. DeLine. Adoption and focus: Practical linear types for imperative programming. In ACM Conference on Programming Language Design and Implementation, pages 13--24, June 2002. Google ScholarDigital Library
- S. Fink, E. Yahav, N. Dor, G. Ramalingam, and E. Geay. Effective typestate verification in the presence of aliasing. In ACM Int. Symposium on Software Testing and Analysis, pages 133--144, July 2006. Google ScholarDigital Library
- C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. Saxe, and R. Stata. Extended static checking for Java. In ACM Conference on Programming Language Design and Implementation, pages 234--245, May 2002. Google ScholarDigital Library
- J. Foster, T. Terauchi, and A. Aiken. Flow-sensitive type qualifiers. In ACM Conference on Programming Language Design and Implementation, pages 1--12, 2002. Google ScholarDigital Library
- D. Giannakopoulou, C. S. Pǎsǎreanu, and J. M. Cobleigh. Assume-guarantee verification of source code with designlevel assumptions. In Int. Conference on Software Engineering, pages 211--220, May 2004. Google ScholarDigital Library
- J.-Y. Girard. Linear logic. Theoretical Computer Science, 50:1--102, 1987. Google ScholarDigital Library
- S. Hallem, B. Chelf, Y. Xie, and D. Engler. A system and language for building system-specific, static analyses. In ACM Conference on Programming Language Design and Implementation, pages 69--82, 2002. Google ScholarDigital Library
- D. Harel. Statecharts: A visual formalism for complex systems. Sci. Comput. Programming, 8:231--274, 1987. Google ScholarDigital Library
- T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In ACM Symposium on Principles of Programming Languages, pages 58--70, 2002. Google ScholarDigital Library
- G. Hughes and T. Bultan. Interface grammars for modular software model checking. In ACM Int. Symposium on Software Testing and Analysis, pages 39--49. ACM Press, July 2007. Google ScholarDigital Library
- A. Igarashi and N. Kobayashi. Resource usage analysis. In ACM Symposium on Principles of Programming Languages, pages 331--342, Jan. 2002. Google ScholarDigital Library
- A. Igarashi, B. Pierce, and P. Wadler. Featherweight Java: A minimal core calculus for Java and GJ. In ACM Conference on Object-Oriented Programming, Systems, Languages & Applications, pages 132--146, 1999. Google ScholarDigital Library
- V. Kuncak, P. Lam, K. Zee, and M. Rinard. Modular pluggable analyses for data structure consistency. IEEE Transactions on Software Engineering, 32(12), Dec. 2006. Google ScholarDigital Library
- G. T. Leavens, A. L. Baker, and C. Ruby. JML: A notation for detailed design. In H. Kilov, B. Rumpe, and I. Simmonds, editors, Behavioral Specifications of Businesses and Systems, pages 175--188. Kluwer Academic Publishers, Boston, 1999.Google ScholarDigital Library
- K. R. M. Leino. Data groups: Specifying the modification of extended state. In ACM Conference on Object-Oriented Programming, Systems, Languages & Applications, pages 144--153, Oct. 1998. Google ScholarDigital Library
- P. Lincoln and A. Scedrov. First-order linear logic without modalities is NEXPTIME-hard. Theoretical Computer Science, 135:139--154, 1994. Google ScholarDigital Library
- B. H. Liskov and J. M. Wing. A behavioral notion of subtyping. ACM Transactions on Programming Languages and Systems, 16(6):1811--1841, Nov. 1994. Google ScholarDigital Library
- Y. Mandelbaum, D. Walker, and R. Harper. An effective theory of type refinements. In ACM Int. Conference on Functional Programming, pages 213--225, 2003. Google ScholarDigital Library
- M. G. Nanda, C. Grothoff, and S. Chandra. Deriving object typestates in the presence of inter-object references. In ACM Conference on Object-Oriented Programming, Systems, Languages & Applications, pages 77--96, 2005. Google ScholarDigital Library
- G. Ramalingam, A. Warshavsky, J. Field, D. Goyal, and M. Sagiv. Deriving specialized program analyses for certifying component-client conformance. In ACM Conference on Programming Language Design and Implementation, pages 83--94, 2002. Google ScholarDigital Library
- F. Smith, D. Walker, and G. Morrisett. Alias types. In European Symposium on Programming, pages 366--381. Springer, 2000. Google ScholarDigital Library
- R. E. Strom and S. Yemini. Typestate: A programming language concept for enhancing software reliability. IEEE Transactions on Software Engineering, 12:157--171, 1986. Google ScholarDigital Library
- G. Tan, X. Ou, and D. Walker. Enforcing resource usage protocols via scoped methods. In Int. Workshop on Foundations of Object-Oriented Languages, 2003.Google Scholar
- P. Wadler. Linear types can change the world! In Working Conference on Programming Concepts and Methods, pages 347--359. North Holland, 1990. Google ScholarDigital Library
Index Terms
- Modular typestate checking of aliased objects
Recommendations
Foundations of Typestate-Oriented Programming
Typestate reflects how the legal operations on imperative objects can change at runtime as their internal state changes. A typestate checker can statically ensure, for instance, that an object method is only called when the object is in a state for which ...
Typestate-like analysis of multiple interacting objects
OOPSLA '08: Proceedings of the 23rd ACM SIGPLAN conference on Object-oriented programming systems languages and applicationsThis paper presents a static analysis of typestate-like temporal specifications of groups of interacting objects, which are expressed using tracematches. Whereas typestate expresses a temporal specification of one object, a tracematch state may change ...
Modular typestate checking of aliased objects
Proceedings of the 2007 OOPSLA conferenceObjects often define usage protocols that clients must follow inorder for these objects to work properly. Aliasing makes itnotoriously difficult to check whether clients and implementations are compliant with such protocols. Accordingly, existing ...
Comments