A graph-based generic type system for object-oriented programs

Abstract

We present a graph-basedmodel of a generic type system for an OO language. The type system supports the features of recursive types, generics and interfaces, which are commonly found in modern OO languages such as Java. In the classical graph theory, we define type graphs, instantiation graphs and conjunction graphs that naturally illustrate the relations among types, generics and interfaces within complex OO programs. The model employs a combination of nominal and anonymous nodes to represent respectively types that are identified by names and structures, and defines graph-based relations and operations on types including equivalence, subtyping, conjunction and instantiation. Algorithms based on the graph structures are designed for the implementation of the type system. We believe that this type system is important for the development of a graph-based logical foundation of a formal method for verification of and reasoning about OO programs.

Keywords

OO programs / type systems / generics / type graphs / recursive types

References

[1] Gosling J, Joy B, Steele G, Bracha G. Java Language Specification: The Java Series. Addison-Wesley Longman Publishing Co., Inc. Boston, MA, USA, 2000

[2] OMG Unified Modeling Language (OMG UML), Superstructure, V2.1.2, 2007. Object Management Group

[3] Hoare C A R, He J. A trace model for pointers and objects. In: Proceedings of the 13th European Conference on Object-Oriented Programming, LNCS 1628. 1999, 1-17

[4] Jifeng H, Li X, Liu Z. rCOS: a refinement calculus of object systems. Theoretical Computer Science, 2006, 365(1): 109-142

[5] Klein G, Nipkow T. A machine-checked model for a Java-like language, virtual machine, and compiler. ACM Transactions on Programming Languages and Systems, 2006, 28(4): 619-695

[6] Ke W, Liu Z, Wang S, Zhao L. A graph-based operational semantics of OO programs. Formal Methods and Software Engineering, 2009, 347-366

[7] Bracha G. Generics in the Java programming language. Sun Microsystemsm, 2004, 1-23

[8] Pierce B. Types and Programming Languages. The MIT Press, 2002

[9] Gauthier N, Pottier F. Numbering matters: first-order canonical forms for second-order recursive types. In: ACM SIGPLAN Notices, 2004, 39(9): 150-161

[10] Ke W, Li X, Liu Z, Stolz V. rCOS: a formal model-driven engineering method for component-based software. Frontiers of Computer Science, 2012, 6(1): 17-39

[11] Zhao L, Liu X, Liu Z, Qiu Z. Graph transformations for object-oriented refinement. Formal Aspects of Computing, 2009, 21(1): 103-131

[12] Ke W, Liu Z, Wang S, Zhao L. Graph-based type system, operational semantics and implementation of an object-oriented programming language. Technical Report 410, UNU-IIST, Macau, China, 2009.

[13] Abadi M, Cardelli L. A theory of objects. Springer, 1996

[14] Igarashi A, Pierce B, Wadler P. Featherweight Java: aminimal core calculus for Java and GJ. ACM Transactions on Programming Languages and Systems, 2001, 23(3): 396-450

[15] Wang S, Long Q, Qiu Z. Type safety for FJ and FGJ. Theoretical Aspects of Computing-ICTAC 2006, 2006, 257-271

[16] Rémy D. From classes to objects via subtyping. Programming Languages and Systems, 1998, 200-220

[17] Igarashi A, Viroli M. On variance-based subtyping for parametric types. In: Proceedings of the 16th European Conference on Object- Oriented Programming. 2002, 441-469

[18] Ferreira A, Foss L, Ribeiro L. Formal verification of object-oriented graph grammars specifications. Electronic Notes in Theoretical Computer Science, 2007, 175(4): 101-114

[19] Corradini A, Dotti F, Foss L, Ribeiro L. Translating Java code to graph transformation systems. Graph Transformations, 2004, 171-174

[20] Kastenberg H, Kleppe A, Rensink A. Defining object-oriented execution semantics using graph transformations. Formal Methods for Open Object-Based Distributed Systems, 2006, 186-201

[21] Heckel R, Küster J, Taentzer G. Confluence of typed attributed graph transformation systems. Graph Transformation, 2002, 161-176

[22] Wermelinger M, Fiadeiro J. A graph transformation approach to software architecture reconfiguration. Science of Computer Programming, 2002, 44(2): 133-155

[23] Ehrig H, Ehrig K, Prange U, Taentzer G. Fundamental theory for typed attributed graphs and graph transformation based on adhesive HLR categories. Fundamenta Informaticae, 2006, 74(1): 31-61

[24] Reacute;my D, Yakobowski B. A graphical presentation of ML F types with a linear-time unification algorithm. In: Proceedings of the 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation. 2007, 27-38

[25] Wright A, Felleisen M. A syntactic approach to type soundness. Information and Computation, 1994, 115(1): 38-94

[26] Flanagan C, Leino K, Lillibridge M, Nelson G, Saxe J, Stata R. Extended static checking for Java. ACM SIGPLAN Notices, 2002, 37(5): 234-245

RIGHTS & PERMISSIONS

Higher Education Press and Springer-Verlag Berlin Heidelberg