Publications

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, 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 graphbased logical foundation of a formal method for verification of and reasoning about OO programs.

Model-driven architecture (MDA) has become a main stream technology for software-intensive system design. The main engineering principle behind it is that the inherent complexity of software development can only be mastered by building, analyzing and manipulating system models. MDA also deals with system complexity by providing component-based design techniques, allowing independent component design, implementation and deployment, and then system integration and reconfiguration based on component interfaces. The model of a system in any stage is an integration of models of different viewpoints. Therefore, for a model-driven method to be applied effectively, it must provide a body of techniques and an integrated suite of tools for model construction, validation, and transformation. This requires a number of modeling notations for the specification of different concerns and viewpoints of the system. These notations should have formally defined syntaxes and a unified theory of semantics. The underlying theory of the method is needed to underpin the development of tools and correct use of tools in software development, as well as to formally verify and reason about properties of systems in mission-critical applications. The modeling notations, techniques, and tools must be designed so that they can be used seamlessly in supporting development activities and documentation of artifacts in software design processes. This article presents such a method, called the rCOS, focusing on the models of a system at different stages in a software development process, their semantic integration, and how they are constructed, analyzed, transformed, validated, and verified.

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, 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 onymous and anonymous nodes to represent respectively types that are identified as names and structures, and defines graph-based relations and operations on types including subtyping, equivalence, 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.

We present a mathematical model of class graphs, object graphs and state graphs which naturally capture the essential oo features. A small-step operational semantics of oo programs is defined in the style of classical structural operational semantics, in which an execution step of a command is defined as a transition from one state graph to another obtained by simple operations on graphs. To validate this semantics, we give it an implementation in Java. This implementation can also be used for simulation and validation of oo programs, with the visualization of state graph transitions during the execution. A distinct feature of this semantics is location or address independent. Properties of objects and oo programs can be described as properties of graphs in terms of relations of navigation paths (or attribute strings).

 We present a graph-based model of a type system and an operational semantics for an object-oriented programming language. In this model, we define class graphs, object graphs and state graphs that naturally capture the essential oo features. The type system checks whether an expression, a command or a program is type-correct, based on its class graph and type context, which is a graph too. The operational semantics is a small-step one defined in the style of classical structural operational semantics, in which an execution step of a command is defined as a transition from one state graph to another obtained by simple operations on graphs. Both the type system and the semantics are fully implemented. On the one hand, working out the implementation has helped us to understand the semantics to make sure our definition is correct. On the other hand, the implementation will be used as the basis for our future development of simulation and validation techniques for oo programs, with the visualization of stage graph transitions during the execution. The motivation of this work is the development of techniques for reasoning about properties of oo programs stated in a logic of graphs. We show the promises and feasibility of this by formulating a range of assertions about objects.