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

作　　者：Wei KE Zhiming LIU Shuling WANG Liang ZHAO 

机构地区：[1]Macao Polytechnic Institute, Macao, China United Nations University [2]International Institute for Software Technology, Macao, China [3]The Institute of Software, Chinese Academy of Sciences, Beijing 100190, China

出　　处：《Frontiers of Computer Science》2013年第1期109-134,共26页中国计算机科学前沿（英文版）

摘　　要：We present a graph-based model 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, instantia- tion graphs and conjunction graphs that naturally iIlustrate 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 de- fines graph-based relations and operations on types including equivalence, subtyping, conjunction and instantiation. Algo- rithms based on the graph structures are designed for the im- plementation 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.We present a graph-based model 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, instantia- tion graphs and conjunction graphs that naturally iIlustrate 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 de- fines graph-based relations and operations on types including equivalence, subtyping, conjunction and instantiation. Algo- rithms based on the graph structures are designed for the im- plementation 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.

关 键 词：OO programs type systems GENERICS type graphs recursive types 

分 类 号：TP312[自动化与计算机技术—计算机软件与理论] TP31[自动化与计算机技术—计算机科学与技术]