Publications

 An object-oriented program consists of a section of class declarations and a main method. The class declaration section represents the structure of an object-oriented program, that is the data, the classes and relations among them. The execution of the main method realizes the application by invoking methods of objects of the classes defined in the class declarations. Class decorations define the general properties of objects and how they collaborate with each other in realizing the application task programmed as the main method. Note that for one class declaration section, different main methods can be programmed for different applications, and this is an important feature of reuse in object-oriented programming. On the other hand, different class declaration sections may support the same applications, but these different class declaration sections can make significant difference with regards to understanding, reuse and maintainability of the applications. With a UML-like modeling language, the class declaration section of a program is represented as a class diagram, and the instances of the class diagram are represented by object diagrams, that form the state space of the program. In this paper, we define a class diagram and its object diagrams as directed labeled graphs, and investigate what changes in the class structure maintain the capability of providing functionalities (or services). We formalize such as structure change by the notion of structure refinement. A structure refinement is a transformation from one graph to another that preserves the capability of providing services, that is, the resulting class graph should be able to provide at least as many, and as good, services (in terms of functional refinement) as the original graph. We then develop a calculus of object-oriented refinement in which the refinement rules are classified into four categories according to their natures and uses in object-oriented software design. The soundness of the calculus is proved and the completeness of the refinement rules of each category is established with regard to normal forms defined for object-oriented programs. These completeness results show the power of the simple refinement rules. The normal forms and the completeness results together capture the essence of polymorphism, dynamic method binding and object sharing by references in object-oriented computation. Keywords: Class graph, Object graph, Graph transformation, Normal form, Object-orientation, Structure refinement.

 An object-oriented program consists of a section of class declarations and a main method. The class declaration section represents the structure of an object-oriented program, that is the data, the classes and relations among them. The execution of the main method realizes the application by invoking methods of objects of the classes defined in the class declarations. Class declarations define the general properties of objects and how they collaborate with each other in realizing the application task programmed as the main method. Note that for one class declaration section, different main methods can be programmed for different applications, and this is an important feature of reuse in object-oriented programming. On the other hand, different class declaration sections may support the same applications, but these different class declaration sections can make significant difference with regards to understanding, reuse and maintainability of the applications. With a UML-like modeling language, the class declaration section of a program is represented as a class diagram, and the instances of the class diagram are represented by object diagrams, that form the state space of the program. In this paper, we define a class diagram and its object diagrams as directed labeled graphs, and investigate what changes in the class structure maintain the capability of providing functionalities (or services). We formalize such a structure change by the notion of structure refinement. A structure refinement is a transformation from one graph to another that preserves the capability of providing services, that is, the resulting class graph should be able to provide at least as many, and as good, services (in terms of functional refinement) as the original graph. We then develop a calculus of object-oriented refinement, as an extension to the classical theory of data refinement, in which the refinement rules are classified into four categories according to their natures and uses in object-oriented software design. The soundness of the calculus is proved and the completeness of the refinement rules of each category is established with regard to normal forms defined for object-oriented programs. These completeness results show the power of the simple refinement rules. The normal forms and the completeness results together capture the essence of polymorphism, dynamic method binding and object sharing by references in object-oriented computation. 

 We have recently developed an object-oriented refinement calculus called rCOS. With rCOS, we formalize the object-orient design principles and patterns as refinement laws. rCOS has been proven to provide formal support to software design and program refactoring. All these features together show that rCOS can be used as a formal framework for the use-cased driven,incremental and iterative Rational Unified Process (RUP). In this paper, we apply rCOS to a step-wised development of a Point of Sale Terminal (POST) system and demonstrate how to apply the refinement laws for design and refactoring, from a requirement model to a design model, and finally, to the implementation in Visual C\#.

An object-oriented program consists of a section of class declarations and a main method. The class declaration section represents the structure of an object-oriented program, that is the data, the classes and relations among them. The execution of the main method realizes the application by invoking methods of objects of the classes defined in the class declarations. Class declarations define the general properties of objects and how they collaborate with each other in realizing the application task programmed as the main method. Note that for one class declaration section, different main methods can be programmed for different applications, and this is an important feature of reuse in object-oriented programming. On the other hand, different class declaration sections may support the same applications, but these different class declaration sections can make significant difference with regards to understanding, reuse and maintainability of the applications. With a UML-like modeling language, the class declaration section of a program is represented as a class diagram, and the instances of the class diagram are represented by object diagrams, that form the state space of the program. In this paper, we define a class diagram and its object diagrams asdirected labeled graphs, and investigate what changes in the class structure maintain the capability of providing functionalities (or services). We formalize such a structure change by the notion of structure refinement. A structure refinement is a transformation from one graph to another that preserves the capability of providing services, that is, the resulting class graph should be able to provide at least as many, and as good, services (in terms of functional refinement) as the original graph. We then develop a calculus of object-oriented refinement, as an extension to the classical theory of data refinement, in which the refinement rules are classified into four categories according to their natures and uses in object-oriented software design. The soundness of the calculus is proved and the completeness of the refinement rules of each category is established with regard to normal forms defined for object-oriented programs. These completeness results show the power of the simple refinement rules. The normal forms and the completeness results together capture the essence of polymorphism, dynamic method binding and object sharing by references in object-oriented computation. 

Being a successful technique in software practice, object orientation (OO) is a hot topic in academic research fields. Among many formalisms, rCOS, a refinement calculus of object-oriented systems based on unifying theories of programming (UTP), has been proven a promising one in the sense of its applications to incremental software constructions, the formal use of UML, etc. However, equipped with a semantics reasoning on both static and dynamic properties, rCOS is not designed for static checking. We believe introducing static checking will extend the power of rCOS. In this paper, we develop a type system for rCOS and prove some type safety theorems. To make the theoretical results of this paper convincible and easy to be understood, we follow the traditional approaches of type systems construction. That is, we use an operational semantics as the basic explanation of rCOS language in spite of the fact that rCOS is originally developed in a denotational framework.