Researchers: | Yuhong Xiong |
---|---|

Advisor: | Edward A. Lee |

Type systems in modern programming language are the most widely used and effective (semi)formal verification tools for software. The theory underlying type systems is simple, robust, and extremely powerful, based on fixed-point theorems in topology. The mathematical structure of a set of types is abstractly a lattice, and the theory can be applied to any property of the software that can be characterized using a lattice. It need not be restricted to classical data types.

In view of this, we have designed a set of Java classes in Ptolemy II that provide support for any type system that can be represented using such a lattice. This generic infrastructure has been first applied to the basic type system problem, that of ensuring consistent data typing, and supporting (polymorphic) type inference. But the infrastructure is designed to be extended to more sophisticated uses.

The basic type system combines static typing with run-time type checking. It supports polymorphic typing of system components, and allows automatic lossless type conversion at run-time. To achieve this, we use a lattice to model the lossless type conversion relation among types, and use inequalities defined over the type lattice to specify type constraints in components and across components. The system of inequalities can be solved efficiently, with existence and uniqueness of a solution guaranteed by fixed-point theorems. This type system increases the safety and flexibility of the design environment, promotes component reuse, and helps simplify component development and optimization.

We are currently developing two extensions. One extension is to add support for structured types such as array and record types. The goal is to allow the elements of arrays and records to contain data tokens of arbitrary types, including structured types, and be able to specify type constraints on them. Type constraints and type inference must propagate transparently across operators that construct and disassemble such structures. One of the major difficulties in this extension is that the type lattice becomes infinite, which raises questions on the convergence of type checks and inference.

A more innovative (and speculative) extension is to *process-level
types*. These types represent dynamic properties of an application,
rather than the static data types traditionally dealt with in a type
system. One of the dynamic properties we have studied is communication
protocol. We have attempted to characterize different communication
protocols as types and describe these types using automata. Furthermore,
we have organized these types into a system-level type lattice using the
simulation relation. This lattice provides significant insight into the
relation between various protocols and may help design polymorphic
components that can work with multiple protocols. For example, we can
specify the behavior of a polymorphic component using a non-deterministic
automaton. If this automaton simulates the automata of some specific
protocols, the component will be able to work with those protocols.

Last updated 11/02/00