my picture GARY T. LEAVENS (Leavens@ucf.edu)

Professor in the University of Central Florida's Department of Computer Science.

(From January 1989 until August 2007, I was a professor of Computer Science at Iowa State University.)

Major Research Interests

Programming and specification language design and semantics, formal methods (program specification and verification), aspect-oriented languages, object-oriented languages, distributed languages, type theory, programming methodology, software engineering, information assurance, computer science education.

Current Research

The long term goal of my research is to better understand how to solve programming problems: how to specify such problems, methods for thinking about such problems, notations for expressing solutions, and ways to check that the solutions are correct. In pursuing this goal, I have worked in two main areas: formal methods and programming languages. formal methods and programming languages.

Formal Methods

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 a large and growing international team of collaborators. 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 with Clyde Ruby reported at OOPSLA 2000 and in his dissertation aims to explain needs to be specified to deriving a subclass without seeing the source code for a superclass. There have also been papers (with Peter Müller and Arnd Poetzsch-Heffter) that use ownership to solve modularity problems in the specification and verification of layered systems. JML has also fostered much interesting work by other researchers. However, there are several important features that need more work, such as concurrency and 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. Early work on JML was done jointly with (former ISU professor) Al Baker, and former Ph.D. student Clyde Ruby. Former Ph.D. student Yoonsik Cheon, designed Larch/Smalltalk, helped in the design of Larch/C++, tools for JML, and is also contributing to the design of JML as an assistant professor at Univ. of Texas, El Paso. Several of my other students have also helped with the JML project. I have also worked 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.

The idea of behavioral subtyping, which I helped develop, supports a programming discipline, supertype abstraction, that solves this problem. 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. Behavioral subtyping makes this technique sound. 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. Recent work with David Naumann (of Stevens) on behavioral subtyping has precisely characterized modular reasoning (supertype abstraction) for Java-like languages with mutation, and formally justifies its soundness. The work with Dhara, Pigozzi, and Naumann on the above topics was funded by various grants from 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.

Programming Language Design and Semantics

The other main aspect of my work has been on the design and semantics of programming languages. This falls in two areas: object-oriented languages with generic functions and aspect-oriented languages.

Languages with generic functions are also 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 (now a professor at Rose-Hulman) and has been done in collaboration with Craig Chambers of the University of Washington and his former Ph.D. student Todd Millstein (now a professor at UCLA). (Students 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 and is featured in an ACM TOPLAS article.

One big problem I worked on (with Craig Chambers) was how to get a language with both a (sound) static type system and a sensible module system. This problem was solved by Millstein and Chambers (as reported in ECOOP '99). We have applied their ideas to the design of an extension to the Java programming language called MultiJava. The ideas also seem applicable to the design of OO languages that are more flexible.

A second interest in programming languages has been in aspect-oriented (AO) languages. As typified by AspectJ, AO languages offer advanced features for modularizing cross-cutting concerns, such as advice and intertype declarations (like MultiJava's ``open classes''). As part of a long term effort to better understand AO languages, my former Ph.D. student Curtis Clifton and I have been working on reasoning (e.g., about correctness) in AO languages. This work has been backed by a study of the operational semantics and type systems of AO languages. Curtis developed a simple and easily understood operational semantics for an AspectJ-like language, with a sound type system. This work also involved an effect system (concern domains) that makes it possible to more efficiently and effectively reason about AO programs. Recent results towards this end (with James Noble) appear in ECOOP 2007. This work also involved an effect system (concern domains) that we hope will make it possible to more efficiently and effectively reason about AO programs.

More recently, Hridesh Rajan and I have been working on a programming language that is less expressive than AspectJ-like languages, but which has advantages for modular reasoning. This language, Ptolemy, is a hybrid of an implicit-invocation language and an aspect-oriented language. It has promise both as a low-level language for virtual machines and for supporting easier static reasoning.

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 funded Curtis's research on AO 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.

Representative Publications

For More Information

See the following for more publications and other information.

Contact Information

Gary T. Leavens
University of Central Florida
College of Engineering and Computer Science
Dept. of Computer Science, 329 L3Harris Center (Building 116)
4000 Central Florida Blvd.,
Orlando, Florida 32816-2362 USA

e-mail: Leavens@ucf.edu
Phone: +1-407-823-4758 / fax: +1-407-823-1488

Last update $Date: 2024/08/09 16:00:20 $