Lightweight confinement for featherweight java

ABSTRACT

Confinement properties impose a structure on object graphs which can be used to enforce encapsulation properties essential to certain program optimizations, modular reasoning, and software assurance. This paper formalizes the notion of confined type in the context of Featherweight Java. A static type system that mirrors the informal rules of Grothoff et al [17] is proven sound. The definition of confined types is extended to confined instantiation of generic classes. This allows for confined collection types in Java and for classes that can be confined post hoc. Confinement type rules are given for Generic Featherweight Java, and proven sound.

REFERENCES

• 1: Paulo Sergio Almeida. Balloon types: Controlling sharing of state in data types. In Mehmet Aksit and Satoshi Matsuoka, editors, ECOOP'97--Object-Oriented Programming, 11th European Conference volume 1241 of LNCS pages 32--59, Jyvaskyla, Finland, 9--13 June 1997. Springer-Verlag.
• 2: Anindya Banerjee , David A. Naumann, Representation independence, confinement and access control [extended abstract], ACM SIGPLAN Notices, v.37 n.1, p.166-177, Jan. 2002
• 3: Chandrasekhar Boyapati , Robert Lee , Martin Rinard, Ownership types for safe programming: preventing data races and deadlocks, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 4: Chandrasekhar Boyapati , Alexandru Salcianu , William Beebee, Jr. , Martin Rinard, Ownership types for safe region-based memory management in real-time Java, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 5: John Boyland , James Noble , William Retert, Capabilities for Sharing: A Generalisation of Uniqueness and Read-Only, Proceedings of the 15th European Conference on Object-Oriented Programming, p.2-27, June 18-22, 2001
• 6: Dave Clarke , Michael Richmond , James Noble, Saving the world from bad beans: deployment-time confinement checking, Proceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications, October 26-30, 2003, Anaheim, California, USA
• 7: David Gerard Clarke, Object ownership and containment, 2003
• 8: David G. Clarke , John M. Potter , James Noble, Ownership types for flexible alias protection, ACM SIGPLAN Notices, v.33 n.10, p.48-64, Oct. 1998
• 9: D. Detlefs, K.Rustan M.Leino, and G. Nelson. Wrestling with rep exposure. Technical report, Digital Equipment Corporation Systems Research Center, 1996.
• 10: Daniela Genius , Martin Trapp , Wolf Zimmermann, An Approach to Improve Locality Using Sandwich Types, Proceedings of the Second International Workshop on Types in Compilation, p.194-214, March 25-27, 1998
• 11: Christian Grothoff , Jens Palsberg , Jan Vitek, Encapsulating objects with confined types, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.241-255, October 14-18, 2001, Tampa Bay, FL, USA
• 12: John Hogg, Islands: aliasing protection in object-oriented languages, Conference proceedings on Object-oriented programming systems, languages, and applications, p.271-285, October 06-11, 1991, Phoenix, Arizona, United States
• 13: John Hogg , Doug Lea , Alan Wills , Dennis deChampeaux , Richard Holt, The Geneva convention on the treatment of object aliasing, ACM SIGPLAN OOPS Messenger, v.3 n.2, p.11-16, April 1992 [doi>10.1145/130943.130947]
• 14: Atsushi Igarashi , Benjamin C. Pierce , Philip Wadler, Featherweight Java: a minimal core calculus for Java and GJ, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.3, p.396-450, May 2001 [doi>10.1145/503502.503505]
• 15: S.J.H. Kent and I. Maung. Encapsulation and Aggregation. In Proceedings of TOOLS PACIFIC 95 (TOOLS 18). Prentice Hall, 1995.
• 16: James Noble , Jan Vitek , John Potter, Flexible Alias Protection, Proceedings of the 12th European Conference on Object-Oriented Programming, p.158-185, July 20-24, 1998
• 17: Jan Vitek , Boris Bokowski, Confined types in Java, Software—Practice & Experience, v.31 n.6, p.507-532, May 2001 [doi>10.1002/spe.369]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features

General Terms:
Languages, Theory, Verification

Keywords:
aliasing, confined types, ownership