Marcelo Sihman, Bar Ilan

Language and Proof Support for Superimpositions and Aspects

Abstract:
A `classic' distributed superimposition is a program module that can augment an
underlying distributed program with added functionality, while cutting across
usual language modularity constructs like processes, packages, or objects. The
ideas of a `classic' distributed superimposition are used to design a new
object-oriented version incorporating aspects, where a superimposition is a
collection of generic parameterized aspects and new classes. The proposed
construct extends the expressiveness and modularity of aspect-oriented
programming (AOP).

Among the new facilities proposed are: grouping related aspects into a
superimposition, extending parameterization of aspects, dealing with
interaction and interference among aspects, combining superimpositions to
obtain new superimpositions, and proving correctness of a superimposition with
aspects, like the validation of applications of aspects and superimpositions.
Two ways of combining superimpositions to create new superimpositions are
presented. In sequential combinations a new superimposition is obtained that is
equivalent to first applying one, and then applying the second to the result.
In merging combinations, it is as if each component superimposition is applied
independently to a basic program, without mutual influences.

Superimpositions are separately declared, specified, and verified. Among the
examples used to demonstrate the approach are versions of the dining
philosopher algorithm, a termination detection algorithm for distributed
systems, and a monitoring superimposition that gathers statistics on basic
objects.

Joint work with Shmuel Katz.