Professor of Computer Science, Iowa State University.
The long term goal of my research is to understand better how to solve programming problems: how to specify such problems, methods for thinking about such problems, notations for expressing solutions, ways to check that the solutions are correct, and tools for automating and assisting with these processes. In pursuing this goal, I have worked in two main areas: formal methods and programming languages.
My work in formal methods has been focused on ways to specify and verify object-oriented (OO) software components. The specification work involves the design and formal description of behavioral interface specification languages (BISLs). BISLs record information about detailed design: the interfaces and functional behavior of program modules. My group has designed a BISL for Smalltalk, called Larch/Smalltalk, a BISL for C++, called Larch/C++ Larch/C++, and, a BISL for Java called JML. Current work focuses on JML, and is being done with an international team of collaborators, in addition to people at ISU. Work on JML focuses on the problem of how to make it expressive enough for documenting existing code; we measure this using both theoretical analysis and case studies. We have made some progress; for example, work reported at OOPSLA 2000 aims to explain needs to be specified to deriving a subclass without seeing the source code for a superclass. However, there is a lot of information that cannot (yet) be recorded, such as performance constraints. Our current work on JML funded by the National Science Foundation (NSF) tries to address some of these issues, as well as issues of practicality and how to deal with multimethods (see below). Early work on JML was done jointly with (former ISU professor) Al Baker, and Clyde Ruby. Yoonsik Cheon, designed Larch/Smalltalk, helped in the design of Larch/C++, and is also contributing to the design of JML as an assistant professor at Univ. of Texas, El Paso. I have also been working with Baker and a former Ph.D. student, Tim Wahls, on executing such specifications.
A long term interest in formal methods for OO software components is behavioral subtyping. The message passing mechanism of OO languages, such as C++ and Java, allows one to easily extend programs by adding new types. This works best if objects of the new types behave like the objects of the old types; the old types are supertypes of the new types, which are called subtypes. How should one reason about programs that use subtyping and message passing? We seek a reasoning method, formalized by specification and verification techniques, that is modular in the sense that when subtypes are added to a program, unchanged modules do not have to be respecified or reverified. Modular reasoning is guaranteed by the technique of supertype abstraction, which relies on behavioral subtyping. To use supertype abstraction, one specifies and verifies code in terms of the static types of expressions written in a program (as usual), uses a type checker to ensure that the static types are supertypes of the run-time types, and then must prove that subtypes obey the specifications of their supertypes. This last condition is behavioral subtyping.
Krishna Kishore Dhara, a former Ph.D. student, has extended the formal theory of behavioral subtyping to types whose instances have time-varying state. Professor Don Pigozzi (now retired from the Mathematics Department at ISU) and I have found an exact algebraic characterization of behavioral subtyping for immutable types. We have also been working on effective techniques for proving behavioral subtyping. Our joint research on the above topics was funded by the NSF.
The potential impact of the work in formal methods is possibly great; it might lead to the engineering of software, instead of hacking. It also seems necessary for high quality software components and reuse. But more realistically, I view my research as trying to formally understand what one needs to think about when documenting and reasoning about a program or program component. This can be of great value for teaching and for the construction of tools, even if people do not use the formalism directly or on a daily basis.
The other main aspect of my work has been on the design and semantics of object-oriented languages with generic functions. Such languages are known as multimethod programming languages, because method calls can dispatch a message send on all arguments, unlike a single-dispatching OO language, such as Smalltalk, C++, or Java. Multimethod languages are interesting because they can more easily express solutions to certain problems in OO programming (binary methods).
My work on multimethod languages is joint with my (former) Ph.D. student Curtis Clifton and has been done in collaboration with Craig Chambers of the University of Washington and his (former) Ph.D. student Todd Millstein. Jianbing Chen and Sevtap Karakoy also have contributed to this work. The work focuses on the semantics and type systems for variants of the Cecil and Java languages. To date we have published papers about an algorithm for type checking such languages with very expressive features (orthogonal inheritance and subtyping), about how to add multimethods to existing languages, and a way to add multimethods to Java. The latter has been developed into the language MultiJava. One big problem is to get a language with both a (sound) static type system and a sensible module system; however, this problem has been solved by Millstein and Chambers (as reported in ECOOP '99). We have applied these ideas to the design of an extension to the Java programming language called MultiJava. We hope to apply this to design OO languages that are more flexible. A long term goal is a language that allows one to program abstract data types in two styles, one of which is easier to extend (as in standard OO languages) and the other of which is easier to reason about. Programmers can use both styles in the same program. Another goal is to extend the kind of modular programming and reasoning techniques that apply to MultiJava to aspect-oriented programs. The potential impact of these research directions might be large if this leads to more flexible, modular, and reusable coding practices. A recent NSF grant is starting to fund research on formal methods for such languages.
Details are available through my selection of representative publications below and through my other WWW pages (especially the the JML papers page). You can also look at my vita.
Last update $Date: 2006/01/20 16:59:07 $