Kevin Bierhoff
Jonathan Aldrich
ABSTRACT
Enforcing compliance to API usage protocols is notoriously hard due to possible aliasing of objects through multiple references. In previous work we proposed a sound, modular approach to checking protocol compliance based on typestates that offers a great deal of flexibility in aliasing. In our approach, API protocols are defined based on typestates. Every reference is associated with a permission, and reasoning about permissions is appropriately conservative for the "degree" of possible aliasing admitted by a permission.
This paper describes Plural, a tool to automatically enforce typestate-based protocols using permissions in Java. API developers can specify protocols with simple annotations on methods and method parameters. A static flow analysis tracks permissions in code that uses specified APIs and issues warnings for possible protocol violations.
- K. Bierhoff and J. Aldrich. Modular typestate checking of aliased objects. In ACM Conference on Object-Oriented Programming, Systems, Languages & Applications, pages 301--320, Oct. 2007. Google Scholar
Digital Library
- J. Boyland. Checking interference with fractional permissions. In International Symposium on Static Analysis, pages 55--72. Springer, 2003. 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
- 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
Index Terms
- PLURAL: checking protocol compliance under aliasing
Recommendations
Modular typestate checking of aliased objects
OOPSLA '07: Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems, languages and applicationsObjects 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 ...
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 ...
Usability Hypotheses in the Design of Plaid
PLATEAU '14: Proceedings of the 5th Workshop on Evaluation and Usability of Programming Languages and ToolsPlaid is a research programming language with a focus on typestate, permissions, and concurrency. Typestate describes ordering constraints on method calls to an object; Plaid incorporates typestate into both its object model and its type system. ...
Comments