×

Universe types for topology and encapsulation. (English) Zbl 1209.68125

de Boer, Frank S. (ed.) et al., Formal methods for components and objects. 6th international symposium, FMCO 2007, Amsterdam, The Netherlands, October 24–26, 2007. Revised lectures. Berlin: Springer (ISBN 978-3-540-92187-5/pbk). Lecture Notes in Computer Science 5382, 72-112 (2008).
Summary: The Universe Type System is an ownership type system for object-oriented programming languages that hierarchically structures the object store; it is used to reason modularly about programs.
We formalise Universe Types for a core subset of Java in two steps: We first define a Topological Type System that structures the object store hierarchically into an ownership tree, and demonstrate soundness of the Topological Type System by proving subject reduction. Motivated by concerns of modular verification, we then present an Encapsulation Type System that enforces the owner-as-modifier discipline; that is, that object updates are initiated by the owner of the object.
The contributions of this paper are, firstly, an extensive type-theoretic account of the Universe Type System, with explanations and complete proofs, and secondly, the clean separation of the topological from the encapsulation concerns.
For the entire collection see [Zbl 1155.68012].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Aldrich, J., Chambers, C.: Ownership domains: Separating aliasing policy from mechanism. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 1–25. Springer, Heidelberg (2004) · doi:10.1007/978-3-540-24851-4_1
[2] Andreae, C., Coady, Y., Gibbs, C., Noble, J., Vitek, J., Zhao, T.: Scoped types and aspects for real-time java. In: Thomas, D. (ed.) ECOOP 2006. LNCS, vol. 4067, pp. 124–147. Springer, Heidelberg (2006) · Zbl 1127.68015 · doi:10.1007/11785477_7
[3] Banerjee, A., Naumann, D.: Representation independence, confinement, and access control. In: Principles of Programming Languages (POPL), pp. 166–177. ACM Press, New York (2002) · Zbl 1323.68352
[4] Boyapati, C.: SafeJava: A Unified Type System for Safe Programming. PhD thesis, MIT (2004)
[5] Boyapati, C., Lee, R., Rinard, M.: Ownership types for safe programming: Preventing data races and deadlocks. In: Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA). ACM, New York (2002)
[6] Boyapati, C., Liskov, B., Shrira, L.: Ownership types for object encapsulation. In: Principles of programming languages (POPL), pp. 213–223. ACM Press, New York (2003) · Zbl 1321.68166
[7] Cameron, N., Drossopoulou, S., Noble, J., Smith, M.: Multiple Ownership. In: Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pp. 441–460. ACM Press, New York (2007)
[8] Clarke, D.: Object Ownership and Containment. PhD thesis, University of New South Wales (2001) · Zbl 0982.68763
[9] Clarke, D., Drossopoulou, S.: Ownership, Encapsulation and the Disjointness of Types and Effects. In: Object-oriented programming, systems, languages, and applications (OOPSLA), pp. 292–310. ACM, New York (2002)
[10] Clarke, D., Potter, J., Noble, J.: Ownership types for flexible alias protection. In: Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), vol. 33(10), pp. 48–64. ACM Press, New York (1998) · Zbl 0924.68038
[11] Cunningham, D., Drossopoulou, S., Eisenbach, S.: Universe Types for Race Safety. In: Verification and Analysis of Multi-threaded Java-like Programs (VAMP), pp. 20–51 (2007)
[12] Dietl, W.: JML2 Eclipse plug-in, http://pm.inf.ethz.ch/research/universes/tools/eclipse/
[13] Dietl, W.: Universe type system tools for Scala, http://pm.inf.ethz.ch/research/universes/tools/scala/
[14] 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) · doi:10.1007/978-3-540-73589-2_3
[15] Dietl, W., Müller, P.: Universes: Lightweight ownership for JML. Journal of Object Technology (JOT) 4(8), 5–32 (2005) · Zbl 05431212 · doi:10.5381/jot.2005.4.8.a1
[16] Dietl, W., Müller, P.: Ownership type systems and dependent classes. In: Foundations of Object-Oriented Languages (FOOL) (2008)
[17] Felleisen, M., Friedman, D.P., Kohlbecker, E., Duba, B.: A syntactic theory of sequential control. Journal of Theoretical Computer Science 52, 205–237 (1987) · Zbl 0643.03011 · doi:10.1016/0304-3975(87)90109-5
[18] Flanagan, C., Qadeer, S.: Types for atomicity. In: Types in Language Design and Implementation (TLDI), pp. 1–12. ACM Press, New York (2003)
[19] Gasiunas, V., Mezini, M., Ostermann, K.: Dependent classes. In: Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pp. 133–152. ACM Press, New York (2007)
[20] Global Computing Proactive Initiative. Mobius: Mobility, Ubiquity and Security. IST-15905, http://mobius.inria.fr/
[21] Klebermaß, M.: An Isabelle formalization of the Universe Type System. Master’s thesis, Technical University Munich and ETH Zurich (2007), http://pm.inf.ethz.ch/projects/student_docs/Martin_Klebermass/
[22] Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Müller, P., Kiniry, J., Chalin, P., Zimmerman, D.M., Dietl, W.: JML reference manual. Department of Computer Science, Iowa State University (2008), http://www.jmlspecs.org
[23] Leino, K.R.M., Müller, P.: Object invariants in dynamic contexts. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 491–516. Springer, Heidelberg (2004) · doi:10.1007/978-3-540-24851-4_22
[24] Lu, Y., Potter, J.: Protecting Representation with Effect Encapsulation. In: Principles of programming languages (POPL), pp. 359–371. ACM Press, New York (2006) · Zbl 1369.68078
[25] Mitchell, J.C., Plotkin, G.D.: Abstract types have existential type. ACM Trans. Program. Lang. Syst. 10(3), 470–502 (1988) · doi:10.1145/44501.45065
[26] Müller, P.: Modular Specification and Verification of Object-Oriented Programs. LNCS, vol. 2262. Springer, Heidelberg (2002) · Zbl 0998.68034 · doi:10.1007/3-540-45651-1
[27] Müller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular invariants for layered object structures. Science of Computer Programming 62, 253–286 (2006) · Zbl 1100.68539 · doi:10.1016/j.scico.2006.03.001
[28] Müller, P., Rudich, A.: Ownership transfer in Universe Types. In: Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), pp. 461–478. ACM Press, New York (2007)
[29] Potanin, A., Noble, J., Clarke, D., Biddle, R.: Generic ownership for generic Java. In: Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), pp. 311–324. ACM Press, New York (2006) · Zbl 1109.68032
[30] Salcianu, A., Rinard, M.C.: Purity and side effect analysis for java programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 199–215. Springer, Heidelberg (2005) · doi:10.1007/978-3-540-30579-8_14
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.