Abstract
Java(X) is a framework for type refinement. It extends Java’s type language with annotations drawn from an algebra X and structural subtyping in terms of the annotations. Each instantiation of X yields a different refinement type system with guaranteed soundness. The paper presents some applications, formalizes a core language, states a generic type soundness result, and sketches the extensions required for the full Java language (without generics).
The main technical innovation of Java(X) is its concept of activity annotations paired with the notion of droppability. An activity annotation is a capability which can grant exclusive write permission for a field in an object and thus facilitates a typestate change (strong update). Propagation of capabilities is either linear or affine (if they are droppable). Thus, Java(X) can perform protocol checking as well as refinement typing. Aliasing is addressed with a novel splitting relation on types.
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
Andreae, C., Noble, J., Markstrum, S., Millstein, T.: A framework for implementing pluggable type systems. In: Proc. 21th ACM Conf. OOPSLA, Portland, OR, pp. 57–74. ACM Press, Portland (2006)
Boyapati, C., Liskov, B., Shrira, L.: Ownership types for object encapsulation. In: Morrisett, G. (ed.) Proc. 30th ACM Symp. POPL, New Orleans, LA, January 2003, pp. 213–223. ACM Press, New York, ACM SIGPLAN Notices (38)1 (2003)
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.T., Retert, W.: Connecting effects and uniqueness with adoption. In: Abadi, M. (ed.) Proc. 32nd ACM Symp. POPL, January 2005, pp. 283–295. ACM Press, New York (2005)
Cardelli, L.: A semantics of multiple inheritance. Information and Computation 76(2/3), 138–164 (1988)
Chin, B., Markstrum, S., Millstein, T.: Semantic type qualifiers. In: Proc. 2005 ACM Conf. PLDI, pp. 85–95. ACM Press, New York (2005)
DeLine, R., Fähndrich, M.: Enforcing high-level protocols in low-level software. In: Proc. 2001 PLDI, Snowbird, UT, June 2001, pp. 59–69. ACM Press, New York, USA (2001)
DeLine, R., Fähndrich, M.: Typestates for objects. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 465–490. Springer, Heidelberg (2004)
Flanagan, C., Freund, S.N.: Type-based race detection for Java (SIGPLAN Notices). In: PLDI. Proceedings of the 2000 ACM SIGPLAN Conference on Programming Language Design and Implementation, Vancouver, British Columbia, Canada, June 2000, vol. 35(5), pp. 219–232. ACM Press, New York (2000)
Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: Proc. 2003 PLDI, pp. 338–349. ACM Press, New York (2003)
Flanagan, C., Sabry, A., Duba, B.F., Felleisen, M.: The essence of compiling with continuations. In: Proc. 1993 PLDI, pp. 237–247, Albuquerque, New Mexico (June 1993)
Flatt, M., Krishnamurthi, S., Felleisen, M.: A programmer’s reduction semantics for classes and mixins. In: Alves-Foss, J. (ed.) Formal Syntax and Semantics of Java. LNCS, vol. 1523, pp. 241–269. Springer, Heidelberg (1999)
Foster, J.S., Terauchi, T., Aiken, A.: Flow-sensitive type qualifiers. In: Proc. 2002 PLDI, Berlin, Germany, June 2002, pp. 1–12. ACM Press, New York (2002)
Freeman, T., Pfenning, F.: Refinement types for ML. In: Proc. PLDI ’91, Toronto, Canada, June 1991, pp. 268–277. ACM Press, New York (1991)
Hofmann, M., Jost, S.: Type-based amortised heap-space analysis. In: Sestoft, P. (ed.) ESOP 2006 and ETAPS 2006. LNCS, vol. 3924, Springer, Heidelberg (2006)
Lam, P., Kuncak, V., Rinard, M.: Crosscutting techniques in program specification and analysis. In: AOSD ’05. Proceedings of the 4th international conference on Aspect-oriented software development, pp. 169–180. ACM Press, New York (2005)
Mandelbaum, Y., Walker, D., Harper, R.: An effective theory of type refinements. In: Shivers, O. (ed.) Proc. Intl. Conf. Functional Programming 2003, Uppsala, Sweden, August 2003, pp. 213–225. ACM Press, New York (2003)
Mitchell, J.C.: Toward a typed foundation for method specialization and inheritance. In: Proc. 17th ACM Symp. POPL, January 1990, pp. 109–124. ACM Press, San Francisco, CA (1990)
Noble, J., Vitek, J., Potter, J.: Flexible alias protection. In: Jul, E. (ed.) ECOOP 1998. LNCS, vol. 1445, pp. 158–185. Springer, Heidelberg (1998)
Odersky, M., Sulzmann, M., Wehr, M.: Type inference with constrained types. Theory and Practice of Object Systems 5(1), 35–55 (1999)
Palsberg, J.: Type-based analysis and applications. In: ACM (ed.) PASTE’01. ACM SIGPLAN – SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, June 09, 2001, pp. 20–27. ACM Press, New York (2001)
Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)
Schrefl, M., Stumptner, M.: Behavior-consistent specialization of object life cycles. ACM Trans. Software Engineering and Methodology 11(1), 92–148 (2002)
Strom, R.E., Yellin, D.M.: Extending typestate checking using conditional liveness analysis. IEEE Trans. Softw. Eng. 19(5), 478–485 (1993)
Strom, R.E., Yemini, S.: Typestate: A programming language concept for enhancing software reliability. IEEE Trans. Softw. Eng. 12(1), 157–171 (1986)
Thiemann, P.: A type safe DOM API. In: Bierman, G., Koch, C. (eds.) DBPL 2005. LNCS, vol. 3774, Springer, Heidelberg (2005)
Walker, D.: Substructural type systems. In: Pierce, B.C. (ed.) Advanced Topics in Types and Programming Languages, ch. 1, MIT Press, Cambridge (2005)
Wright, A., Felleisen, M.: A syntactic approach to type soundness. Information and Computation 115(1), 38–94 (1994)
Xi, H., Pfenning, F.: Dependent types in practical programming. In: Aiken, A. (ed.) Proc. 26th ACM Symp. POPL, San Antonio, Texas, January 1999, pp. 214–227. ACM Press, New York (1999)
Zhao, T., Palsberg, J., Vitek, J.: Lightweight confinement for Featherweight Java. In: Proc. 18th ACM Conf. OOPSLA, Anaheim, CA, USA, 2003, pp. 135–148. ACM Press, New York (2003)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Degen, M., Thiemann, P., Wehr, S. (2007). Tracking Linear and Affine Resources with Java(X) . In: Ernst, E. (eds) ECOOP 2007 – Object-Oriented Programming. ECOOP 2007. Lecture Notes in Computer Science, vol 4609. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73589-2_26
Download citation
DOI: https://doi.org/10.1007/978-3-540-73589-2_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73588-5
Online ISBN: 978-3-540-73589-2
eBook Packages: Computer ScienceComputer Science (R0)