****************************************************
* Gary T. Leavens provided this position statement *
****************************************************

I'm doing research, with my Ph.D. student Curtis Clifton, in the
general area of reasoning about aspect-oriented systems.  We were
originally interested in how to specify and verify aspect-oriented
programs.  We have written some influential papers on modular
reasoning, obliviousness, and aspect oriented languages.  We noticed,
for example as reported in the 2003 SPLAT workshop, there is an
analogy between method dispatch in object-oriented languages and the
application of the device and aspect-oriented languages.  One way to
obtain modular reasoning in object-oriented languages is to use the
concept of behavioral subtyping.  Our "behavioral subtyping analogy"
seeks a comparable notion for aspect-oriented languages.  However,
this seems difficult for a number of reasons, in part because people
use advice in ways that are intentionally supposed to change the
behavior of a program instead of refining its existing behavior.

We also made a proposal to make aspect-oriented languages like AspectJ
more modular by making a distinction between two different kinds of
aspects.  The first, we called "assistants" are unrestricted, like the
aspects in AspectJ, however their advice had to be explicitly
accepted.  The second, we called "spectators" (or "observers" in an
earlier version of our work) were supposed to be free of side effects,
but in turn their advice could be applied in a completely oblivious
manner.  One problem with this proposal, however, was that it is
difficult to both precisely specify what a spectator is, and to
enforce it.  Furthermore, in an imperative language, it seems useless
to have spectators that can have no side effects.  Finally, this
proposal doesn't seem to follow the spirit of aspect oriented
languages very well, because it seems to give up too much
obliviousness.

For this reason, we have, lately, been investigating a different
approach to trying to achieve some semblance of modular reasoning and
aspect-oriented languages.  We have spent considerable time laying the
theoretical foundations for our work, by modeling the semantics of
aspect-oriented languages like AspectJ using any operational
semantics.  We've also investigated typing issues for these languages.
One interesting issue is the exact typing of AspectJ's "proceed"
construct.  Another issue is how to model replacement of the target
object in a call, which AspectJ permits.

I'm also very interested in formal methods in general, and
specification language design in particular.  Much of my research
centers on the JML specification language, a behavioral interface
specification language tailored to Java.  We are interested in
possible extensions of this work to AspectJ.


         Gary T. Leavens
         Department of Computer Science, Iowa State University
         229 Atanasoff Hall, Ames, Iowa 50011-1041 USA
         http://www.cs.iastate.edu/~leavens  phone: +1-515-294-1580