|
|
|
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 |
|
|
|
|
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
|
|
| 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
|
|
Viewed |
|
|
|
Full text
|
|
|
|
|
Abstract
|
|
|
|
|
Cited |
|
|
|
|
| |
Shared |
|
|
|
|
| |
Discussed |
|
|
|
|
