Please wait a minute...
Frontiers of Computer Science

ISSN 2095-2228

ISSN 2095-2236(Online)

CN 10-1014/TP

Postal Subscription Code 80-970

2018 Impact Factor: 1.129

Front Comput Sci    2013, Vol. 7 Issue (1) : 109-134    https://doi.org/10.1007/s11704-012-1307-8
RESEARCH ARTICLE
A graph-based generic type system for object-oriented programs
Wei KE1, Zhiming LIU2, Shuling WANG3, Liang ZHAO2()
1. Macao Polytechnic Institute, Macau, China; 2. United Nations University – International Institute for Software Technology,Macau, China; 3. The Institute of Software, Chinese Academy of Sciences, Beijing 100190, China
 Download: PDF(754 KB)   HTML
 Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks
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     
Corresponding Author(s): ZHAO Liang,Email:liang@iist.unu.edu   
Issue Date: 01 February 2013
 Cite this article:   
Wei KE,Zhiming LIU,Shuling WANG, et al. A graph-based generic type system for object-oriented programs[J]. Front Comput Sci, 2013, 7(1): 109-134.
 URL:  
https://academic.hep.com.cn/fcs/EN/10.1007/s11704-012-1307-8
https://academic.hep.com.cn/fcs/EN/Y2013/V7/I1/109
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
doi: 10.1016/j.tcs.2006.07.034
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
doi: 10.1145/1146809.1146811
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
doi: 10.1145/1016848.1016872
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
doi: 10.1007/s00165-007-0067-y
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. www.iist.unu.edu/www/docs/techreports/reports/report410.pdf
13 Abadi M, Cardelli L. A theory of objects. Springer , 1996
doi: 10.1007/978-1-4419-8598-9
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
doi: 10.1145/503502.503505
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
doi: 10.1016/j.entcs.2007.04.020
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
doi: 10.1016/S0167-6423(02)00036-9
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
doi: 10.1006/inco.1994.1093
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
doi: 10.1145/543552.512558
[1] Baojian HUA. Static typing for a substructural lambda calculus[J]. Front Comput Sci Chin, 2011, 5(3): 369-380.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed