Concerning Efficient Reasoning in AspectJ-like Languages
			
				  by
			   Gary T. Leavens
	Department of Computer Science, Iowa State University

                                Abstract

Advice in the dynamic aspect-oriented language AspectJ helps
programmers modularize crosscutting concerns by allowing additions and
changes to a program's execution.  However, formal 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 proposed in the literature 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.cs.iastate.edu/~leavens/modular-aop/ .