We present a first instantiation of the general framework for AOP introduced in the previous section. This instantiation, inspired by the work presented in [9], is intended to illustrate two main points:
The usefulness of expressive aspect definitions
The application of general proof techniques for the analysis and transformation of AO programs
Crosscuts In this section, we instantiate the general framework by allowing crosscuts C to be arbitrary predicates. For instance, a predicate isWeakPassword could recognize the event of changing a password to a word a dictionary. Note that we do not define the language of crosscuts; they are to be defined using some general-purpose language.
Stateful Aspects Aspects are defined as a collection of mutually recursive definitions of the form var = A. Since one of our main interests lies in the definition of stateful crosscuts, we base an aspect definition on the following grammar:
A ::= CA1;A2 ; sequence | A1var ; invocation
The grammar allows us to compose aspects by sequentialization, deterministic choice, and aspect invocation. In a deterministic choice A1A1is always chosen if it is applicable; A2 is chosen only if it is applicable, and A1 is not. Using composed aspects, we can define, for example, an aspect tryOnce trying to apply C tryOnce = (Cvoid) void = isAnyskip ;If C matches the current join point, the weaver chooses the first branch and executes the insert I, and the aspect becomes void that keeps doing nothing. Otherwise, the weaver chooses the second branch (void), which keeps doing nothing right from the start.
In order to illustrate how such expressive aspects may be used, consider the following definition:
log = (isLoginaddLog(isLogoutskip) skip isLoginskip ; log ; The aspect logNestedLogin considers sessions starting with a call to the login function with the user identifier as a parameter (whose occurrence is matched by the crosscut isLogin) and ending with a call to the function logout (matched by the crosscut isLogout). This aspect logs nested (i.e., non top-level) calls to the login function, which may be useful because such a call may log into a non-local network and be therefore dangerous. The recursive definition of the aspect is responsible for pairing logins and logouts, thus detecting non top-level calls to login.
Now, let us consider the following aspect:
initAtFirstLogin = isLogininitNetworkInfo() ; This aspect initAtFirstLogin detects the first call to login in order to initialize network information. Then the following calls to login are ignored.
It is easy to prove that the two aspects logNestedLogin and initAtFirstLogin are equivalent to a single sequential aspect. Basically, this can be proven by unfolding recursive definitions and induction principles [9]. The proof starts with a parallel composition logNestedLogin || initAtFirstLogin and eliminates the parallel operator by producing all the possible pairs of crosscuts from the two aspect definitions and by folding. The resulting sequential aspect can be simplified if a pair of crosscuts has no solution. In our example we get the following sequential aspect:
