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 Ja...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.展开更多
Hardware and software co-design is a design technique which delivers computer systems comprising hardware and software components. A critical phase of the co-design process is to decompose a program into hardware and ...Hardware and software co-design is a design technique which delivers computer systems comprising hardware and software components. A critical phase of the co-design process is to decompose a program into hardware and software. This paper proposes an algebraic partitioning algorithm whose correctness is verified in program algebra. The authors introduce a program analysis phase before program partitioning and develop a collection of syntax-based splitting rules. The former provides the information for moving operations from software to hardware and reducing the interaction between components, and the latter supports a compositional approach to program partitioning.展开更多
In this paper, the problem of checking a timed automaton for a Duration Cal-culus formula of the form Temporal Duration Property is addressed. It is shown that TemporalDuration Properties are in the class of discretis...In this paper, the problem of checking a timed automaton for a Duration Cal-culus formula of the form Temporal Duration Property is addressed. It is shown that TemporalDuration Properties are in the class of discretisable real-time properties of Timed Automata,and an algorithm is given to solve the problem based on linear programming techniques andthe depth-first search method in the integral region graph of the automaton. The complexityof the algorithm is in the same class as that of the solution of the reachability problem of timedautomata.展开更多
文摘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.
文摘Hardware and software co-design is a design technique which delivers computer systems comprising hardware and software components. A critical phase of the co-design process is to decompose a program into hardware and software. This paper proposes an algebraic partitioning algorithm whose correctness is verified in program algebra. The authors introduce a program analysis phase before program partitioning and develop a collection of syntax-based splitting rules. The former provides the information for moving operations from software to hardware and reducing the interaction between components, and the latter supports a compositional approach to program partitioning.
文摘In this paper, the problem of checking a timed automaton for a Duration Cal-culus formula of the form Temporal Duration Property is addressed. It is shown that TemporalDuration Properties are in the class of discretisable real-time properties of Timed Automata,and an algorithm is given to solve the problem based on linear programming techniques andthe depth-first search method in the integral region graph of the automaton. The complexityof the algorithm is in the same class as that of the solution of the reachability problem of timedautomata.
