Abstract
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 the operation is well-defined. Prior work has shown how modular typestate checking can be achieved thanks to access permissions and state guarantees. However, static typestate checking is still too rigid for some applications.
This paper formalizes a nominal object-oriented language with mutable state that integrates typestate change and typestate checking as primitive concepts. In addition to augmenting the types of object references with access permissions and state guarantees, the language extends the notion of gradual typing to account for typestate: gradual typestate checking seamlessly combines static and dynamic checking by automatically inserting runtime checks into programs. A novel flow-sensitive permission-based type system allows programmers to write safe code even when the static type checker can only partly verify it.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Ahmed, A., Fluet, M., Morrisett, G.: L3: A linear language with locations. Fundamenta Informaticae 77(4), 397–449 (2007)
Aldrich, J., Sunshine, J., Saini, D., Sparks, Z.: Typestate-oriented programming. In: Proc. Onward! 2009, pp. 1015–1022. ACM, New York (2009)
Baker, H.G.: Minimizing reference count updating with deferred and anchored pointers for functional data structures. SIGPLAN Not. 29, 38–43 (1994)
Bierhoff, K., Aldrich, J.: Modular typestate checking of aliased objects. In: Proc. Conference on Object-oriented Programming Systems and Applications, pp. 301–320. ACM, New York (2007)
Bierhoff, K., Beckman, N.E., Aldrich, J.: Practical API protocol checking with access permissions. In: Drossopoulou, S. (ed.) ECOOP 2009. LNCS, vol. 5653, pp. 195–219. Springer, Heidelberg (2009)
Bierman, G., Meijer, E., Torgersen, M.: Adding dynamic types to c\(^\sharp\). In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 76–100. Springer, Heidelberg (2010)
Bodden, E.: Efficient hybrid typestate analysis by determining continuation-equivalent states. In: Proc. International Conference on Software Engineering, pp. 5–14. ACM, New York (2010)
Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55–72. Springer, Heidelberg (2003)
Boyland, J., Retert, W.: Connecting effects and uniqueness with adoption. In: Symposium on Principles of Programming Languages, pp. 283–295. ACM, New York (2005)
DeLine, R., Fähndrich, M.: Typestates for objects. In: Vetta, A. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 465–490. Springer, Heidelberg (2004)
Drossopoulou, S., Damiani, F., Dezani-Ciancaglini, M., Giannini, P.: Fickle: Dynamic object re-classification. In: Lee, S.H. (ed.) ECOOP 2001. LNCS, vol. 2072, Springer, Heidelberg (2001)
Fink, S.J., Yahav, E., Dor, N., Ramalingam, G., Geay, E.: Effective typestate verification in the presence of aliasing. ACM Trans. Softw. Eng. Methodol. 17(2), 1–34 (2008)
Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Professional Computing Series. Addison-Wesley, Reading (1994)
Garcia, R., Wolff, R., Tanter, É., Aldrich, J.: Featherweight Typestate. Technical Report CMU-ISR-10-115, Carnegie Mellon University (July 2010)
Gay, S., Vasconcelos, V., Ravara, A., Gesbert, N., Caldeira, A.: Modular session types for distributed object-oriented programming. In: Symposium on Principles of programming languages, pp. 299–312. ACM, New York (2010)
Girard, J.-Y.: Linear logic. Theor. Comput. Sci. 50(1), 1–102 (1987)
Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: a minimal core calculus for Java and GJ. ACM Trans. Program. Lang. Syst. 23(3), 396–450 (2001)
Knowles, K., Flanagan, C.: Hybrid type checking. ACM Trans. Program. Lang. Syst. 32(2), 6:1–6:34 (2010)
Levanoni, Y., Petrank, E.: An on-the-fly reference-counting garbage collector for Java. ACM Trans. Program. Lang. Syst. 28, 1–69 (2006)
Naeem, N.A., Lhoták, O.: Typestate-like analysis of multiple interacting objects. In: Proc. Conference on Object-oriented programming systems languages and applications, pp. 347–366. ACM, New York (2008)
Pierce, B.C., Turner, D.N.: Local type inference. ACM Trans. Program. Lang. Syst. 22(1), 1–44 (2000)
Sabry, A., Felleisen, M.: Reasoning about programs in continuation-passing style. Lisp Symb. Comput. 6(3-4), 289–360 (1993)
Saini, D., Sunshine, J., Aldrich, J.: A theory of typestate-oriented programming. In: Formal Techniques for Java-like Programs (2010)
Siek, J.G., Taha, W.: Gradual typing for objects. In: Bateni, M. (ed.) ECOOP 2007. LNCS, vol. 4609, pp. 2–27. Springer, Heidelberg (2007)
Siek, J., Taha, W.: Gradual typing for functional languages. In: Proc. Scheme and Functional Programming Workshop (September 2006)
Strom, R.E., Yemini, S.: Typestate: A programming language concept for enhancing software reliability. IEEE Trans. Softw. Eng. 12(1), 157–171 (1986)
Walker, D.: Substructural type systems. In: Pierce, B. (ed.) Advanced Topics in Types and Programming Languages, ch. 1, pp. 3–43. MIT Press, Cambridge (2005)
Wolff, R., Garcia, R., Tanter, É., Aldrich, J.: Gradual Featherweight Typestate. Technical Report CMU-ISR-10-116R, Carnegie Mellon University (July 2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wolff, R., Garcia, R., Tanter, É., Aldrich, J. (2011). Gradual Typestate. In: Mezini, M. (eds) ECOOP 2011 – Object-Oriented Programming. ECOOP 2011. Lecture Notes in Computer Science, vol 6813. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22655-7_22
Download citation
DOI: https://doi.org/10.1007/978-3-642-22655-7_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22654-0
Online ISBN: 978-3-642-22655-7
eBook Packages: Computer ScienceComputer Science (R0)