Concerning Efficient Reasoning in AspectJ-like Languages
Speaker: Gray Leavens
Date and Time: November 13, 2007, 11:00AM-12:00PM
Room: HEC 101
Abstract
How to modularize code in the face of cross-cutting concerns is a pressing problem for large software systems. Aspect-oriented languages, such as AspectJ, help solve this problem by allowing additions and changes to a program's execution. However, reasoning about the functional behavior of AspectJ code is inefficient, because there is no way to limit potential interference. This leads to whole-program reasoning, despite the sparse nature of actual interference between advice and advice and base program code. After describing these problems, I will give an overview of various techniques for solving them. Some annotations and static analysis can be helpful in allowing efficient reasoning, by identifying what advice is potentially relevant to a given property. In particular I discuss joint work with Clifton and Noble on concern domains, an effect analysis that uses annotations to efficiently identify potential interference. I discuss some situations in which such knowledge can lead to efficient combination of specifications in some situations. I also discuss future work on problems in weaving specifications.
This talk in part describes joint work with Curtis Clifton and James Noble and is based on work described in Clifton's Ph.D. dissertation. That work was supported in part by the US NSF under grant CCF-04-8078. For more details see http://www.eecs.ucf.edu/~leavens/modular-aop/ .
Bio
Gary T. Leavens is a professor in the School of Electrical Engineering and Computer Science at the University of Central Florida, where he has been since August 2007. Previously he was a professor of computer science at Iowa State University in Ames, Iowa, where he started in January 1989. He also received his Ph.D. from MIT in 1989. Before his graduate studies at MIT, he worked at Bell Telephone Laboratories in Denver Colorado as a member of technical staff.
Professor Leavens's research interests include programming and specification language design and semantics, program verification, and formal methods, with an emphasis on the object-oriented and aspect-oriented paradigms. His best known work in the area of formal methods is related to the JML project, an international effort with many associated tools (see jmlspecs.org). He also worked on the design of the specification languages Larch/Smalltalk (with Yoonsik Cheon) and Larch/C++ (with Yoonsik and Clyde Ruby). These languages embody insights from his work on the theory of behavioral subtyping (with Don Pigozzi and Krishna Kishore Dhara). His best known work on language design and semantics is related to multiple dispatch languages (joint with Craig Chambers, Todd Millstein, and Curtis Clifton) such as MultiJava.
See http://www.eecs.ucf.edu/~leavens for more information on his research. His hobbies include music and astronomy. He is married to Janet Leavens, who is a Ph.D. candidate in French Literature at the University of Iowa and a temporaray assistant professor at the University of Central Florida.
