Abstract
We present a type system for checking object immutability, read-only references, and class immutability in an open or closed world. To allow object initialization outside object constructors (which is often needed in practice), immutable objects are initialized in lexically scoped regions. The system is simple and direct; its only type qualifiers specify immutability properties. No auxiliary annotations, e.g., ownership types, are needed, yet good support for deep immutability is provided. To express object confinement, as required for class immutability in an open world, we use qualifier polymorphism. The system has two versions: one with explicit specification commands that delimit the object initialization phase, and one where such commands are implicit and inferred. In the latter version, all annotations are compatible with Java’s extended annotation syntax, as proposed in JSR 308.
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.
References
Barnett, M., DeLine, R., Fähndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology 3(6), 27–56 (2004)
Bierhoff, K., Aldrich, J.: Modular typestate verification of aliased objects. In: OOPSLA, pp. 301–320 (2007)
Bloch, J.: Effective Java. Addison-Wesley, Reading (2001)
Boyapati, C.: SafeJava: A Unified Type System for Safe Programming. Ph.D thesis, MIT (2004)
Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55–72. Springer, Heidelberg (2003)
Boyland, J., Noble, J., Retert, W.: Capabilities for sharing: A generalisation of uniqueness and read-only. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol. 2072, pp. 2–27. Springer, Heidelberg (2001)
Boyland, J., Retert, W.: Connecting effects and uniqueness with adoption. In: POPL, pp. 283–295 (2005)
Clarke, D., Potter, J., Noble, J.: Ownership types for flexible alias protection. In: OOPSLA, pp. 48–64 (1998)
Clarke, D., Wrigstad, T.: External uniqueness is unique enough. In: Cardelli, L. (ed.) ECOOP 2003. LNCS, vol. 2743, pp. 176–200. Springer, Heidelberg (2003)
Crary, K., Walker, D., Morrisett, G.: Typed memory management in a calculus of capabilities. In: POPL, pp. 262–275 (1999)
DeLine, R., Fähndrich, M.: Enforcing high-level protocols in low-level software. In: PLDI, pp. 59–69 (2001)
Dietl, W., Drossopoulou, S., Müller, P.: Generic universe types. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol. 4609, pp. 28–53. Springer, Heidelberg (2007)
Fähndrich, M., Leino, K.R.M.: Declaring and checking non-null types in an object-oriented language. In: OOPSLA, pp. 302–312. ACM Press, New York (2003)
Fähndrich, M., Xia, S.: Establishing object invariants with delayed types. In: OOPSLA, pp. 337–350. ACM, New York (2007)
Felleisen, M., Friedman, D.: A Little Java, A Few Patterns. MIT Press, Cambridge (1997)
Grossman, D., Morrisett, G., Jim, T., Hicks, M., Wang, Y., Cheney, J.: Region-based memory management in Cyclone. In: PLDI, pp. 282–293 (2002)
Haack, C., Poll, E.: Type-based object immutability with flexible initialization. Technical Report ICIS-R09001, Radboud University, Nijmegen (January 2009)
Haack, C., Poll, E., Schäfer, J., Schubert, A.: Immutable objects for a Java-like language. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 347–362. Springer, Heidelberg (2007)
JSR 308 Expert Group. Annotations on Java types. Java specification request, Java Community Process (December 2007)
Leino, K.R.M., Müller, P., Wallenburg, A.: Flexible immutability with frozen objects. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol. 5295, pp. 192–208. Springer, Heidelberg (2008)
Müller, P., Poetzsch-Heffter, A.: Universes: A type system for alias and dependency control. Technical Report 279, Fernuniversität Hagen (2001)
Östlund, J., Wrigstad, T., Clarke, D., Åkerblom, B.: Ownership, uniqueness, and immutability. In: TOOLS Europe, pp. 178–197 (2008)
Papi, M., Ali, M., Correa, T., Perkins, J., Ernst, M.: Practical pluggable types for Java. In: International Symposium on Software Testing and Analysis, pp. 201–212 (2008)
Pechtchanski, I., Sarkar, V.: Immutability specification and applications. Concurrency and Computation: Practice and Experience 17, 639–662 (2005)
Porat, S., Biberstein, M., Koved, L., Mendelson, B.: Automatic detection of immutable fields in Java. In: CASCON 2002. IBM Press (2000)
Potanin, A., Noble, J., Clarke, D., Biddle, R.: Featherweight generic confinement. J. Funct. Program. 16(6), 793–811 (2006)
Potanin, A., Noble, J., Clarke, D., Biddle, R.: Generic ownership for generic Java. In: OOPSLA, pp. 311–324 (2006)
Qi, X., Myers, A.: Masked types for sound object initialization. In: POPL. ACM, New York (2009)
Smith, F., Walker, D., Morrisett, G.: Alias types. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol. 1782, pp. 366–381. Springer, Heidelberg (2000)
Tofte, M., Talpin, J.-P.: Region-based memory management. Information and Computation 132(2), 109–176 (1997)
Unkel, C., Lam, M.: Automatic inference of stationary fields: a generalization of Java’s final fields. In: POPL, pp. 183–195. ACM, New York (2008)
Vitek, J., Bokowski, B.: Confined types in Java. Softw. Pract. Exper. 31(6), 507–532 (2001)
Wrigstad, T.: Ownership-Based Alias Management. Ph.D thesis, KTH Stockholm (2006)
Zibin, Y., Potanin, A., Ali, M., Artzi, S., Kieżun, A., Ernst, M.: Object and reference immutability using Java generics. In: ESEC/FSE 2007, pp. 75–84. ACM, New York (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Haack, C., Poll, E. (2009). Type-Based Object Immutability with Flexible Initialization. In: Drossopoulou, S. (eds) ECOOP 2009 – Object-Oriented Programming. ECOOP 2009. Lecture Notes in Computer Science, vol 5653. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-03013-0_24
Download citation
DOI: https://doi.org/10.1007/978-3-642-03013-0_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-03012-3
Online ISBN: 978-3-642-03013-0
eBook Packages: Computer ScienceComputer Science (R0)