Publications

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).

Simpson’s four-slot algorithm has been an instructive example in studying various assertional proof methods/logics geared towards shared variable concurrency. Previously, techniques like rely-guarantee, data refinement and resource separation have been applied to simplify the construction of its correctness proof. Still, an elegant, concise and insightful proof is elusive. Recently with the new generation of logics coming of age which are, for the first time, equipped with ownership transfer, it becomes imperative to ask to what extent can ownership transfer facilitate a nice proof of the algorithm. Ownership transfer is especially promising here because the conflict resolution mechanism in the four-slot algorithm can be easily recast as an implementation based on ownership transfer.

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.

The refinement calculus provides a methodology for transforming an abstract specification into a concrete implementation, by following a succession of refinement rules. These rules have been mechanized in theorem-provers, thus providing a formal and rigorous way to prove that a given program refines another one. In a previous work, we have extended this mechanization for object-oriented programs, where the memory is represented as a graph, and we have integrated our approach within the rCOS tool, a model-driven software development tool providing a refinement language. Hence, for any refinement step, the tool automatically generates the corresponding proof obligations and the user can manually discharge them, using a provided library of refinement lemmas. In this work, we propose an approach to automate the search of possible refinement rules from a program to another, using the rewriting tool Maude. Each refinement rule in Maude is associated with the corresponding lemma in Isabelle, thus allowing the tool to automatically generate the Isabelle proof when a refinement rule can be automatically found. The user can add a new refinement rule by providing the corresponding Maude rule and Isabelle lemma.

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 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.

This paper presents an approach for the automated generation of proof obligations for OO program refinement defined in the rCOS language. We first extend the mechanization of the refinement calculus done by von Wright in HOL, representing the state of a program as a graph instead of a tuple, in order to deal with object-orientation. The state graph structure is implemented in Isabelle, together with definitions and lemmas, to help the manipulation of states. We then show how proof obligations are automatically generated from the rCOS tool that can be loaded in Isabelle to be proved. We illustrate our approach by generating the proof obligations for a simple example, including object access and method invocation.

 The paper presents a compositional proof outline of Simpson four-slot algorithm using RGSep logic, a combination of rely/guarantee method with separation logic. In the proof, we illustrate the importance of the ownership transfer facility provided by RGSep to achieve non-interferent accesses on data slots by the reader and writer.