To express the general form of the LoD, 
we formulate a relational structure PS that models
program structures sufficiently well to express the LoD. 
PS models LoD as a join point predicate.
We will then use PS to derive both the 

A program structure PS consists of a set of modules.
Each module consists of a name and a set of members.
There are three kinds of members: field, method and constructor.
A field is a member that is associated with a module through a field name.
A method is a tuple (name, argumentModules, returnModule, body).
argumentModules consists of zero or more modules. returnModule is a module
that is optional.
The body consists of a set of join points, each consisting of
a tuple (enclosing, this, target, member, returned),
where enclosing is the enclosing method to which the body belongs; this is the enclosing module
of the method to which the body belongs; 
target is a module and member is a member of target and returned
is the module returned by the member.
A constructor is a special kind of method where the returnModule
is always the enclosing module to which the constructor belongs.

The LoD is a predicate on join points that are presented as a stream 
of join points.
A join point (enclosing, this, target, member, *) in a stream of join points satisfies LoD iff 
(1) target is an element of fields(this) or
(2) target is an element of arguments(enclosing) or
(3) target appeared in an earlier join point of the form (enclosing, this, this, *, target) or
(4) target appeared in an earlier join point of the form (enclosing, this, *, C, target) where
C is a constructor.

fields(this) is the set of modules in fields of module this.
arguments(enclosing) is the set of modules that are arguments of method enclosing.

(1) is module-sensitive and (2)-(4) are method-sensitive.

At any point during the testing of a stream of join points we maintain the
set of potential preferred target modules which are the target modules determined
by conditions (1)-(4). The potential preferred target modules that
are actually used in the method body are called preferred target modules.

GF (General Form):
A stream of join points satisfies the LoD if the targets of all
join points are preferred.

Next we define two interpretations of GF:

Interpretation 1: for a program P: SCF (Static Class Form)
modules = classes.
The join point stream consists of lexical join points in the 
program text. A suitable ordering has to be given: 
traverse through all method definitions and for each method
body enumerate all constructor calls, self calls, followed by the
other join points.


Interpretation 2: for a program P and input I: DOF (Dynamic Object Form)
modules = objects.
The join point stream consists of dynamic join points produced
by the execution of the program.

For a program P and execution E(P,I) for some input I,
we consider the set of lexical join points
according to interpretation 1 and the set of dynamic join points
according to interpretation 2 and we define a function, called Shadow,
that maps a dynamic join point to its lexical shadow \cite{}.
For a dynamic join point d, Shadow(d) returns the static part of d.
We define an equivalence relation etc. (from 3.1).

We view (1) and (3) as operators on join  point predicates.
apply (1) SCF = DCF
apply (3) OF = SOf

(Only five join point predicates! OOF, SCF, DOF, DCF, SOF)
In Figure 1 we use also CF and OF.

We want to check DOF using AspectJ. An OF checker could not be done easily
without an AO language. We believe that AspectJ is the first 
programming language that makes it relatively easy to check DOF.
For designing the checker,
the AspectJ join point model needs to be linked to DOF.

A join point model consists of a set of join points, a means
of specifying a set of join points and a means of specifying
additional information at a set of join points. AspectJ
uses two kinds of join point models: a dynamic one where the join points
are points in the execution of a program and a static one 
where the join points are classes. AspectJ has
excellent support for the dynamic object model, but 
only limited
support for a join point model according to interpretation 1 above.
For example, in the dynamic join point model we can easily
talk about all method calls happening during
the execution of a program by writing "call(* *(..))".
However, we cannot easily express in AspectJ the set of
all MethodCall-objects contained in a given Program-object by using 
a notation like: Shadow(call(* *(..)).

What is missing in AspectJ is that it does not expose the meta
model of AspectJ in the form of a class graph and an abstract syntax
tree and that it does not offer navigational capabilities in 
the meta model commensurate with the navigational capabilities
in the dynamic model.

One justification why AspectJ should not expose the meta model
is that we could just use Java to parse an AspectJ program
and process the abstract syntax tree to check SCF. But 
a parser for AspectJ is already in the AspectJ compiler ready
to be reused. Another justification why AspectJ should not expose
the meta model is that the static join points don't need
enhancement (advice) as opposed to the dynamic join points that
need checking logic to be added. But the meta-level program can be viewed
as a base-level program and we would like to have all the capabilities
of AspectJ to process the meta-level objects (abstract syntax trees).

See
/proj/adaptive/www/papers/law-of-demeter/checker/vision-dynamic-static
for the design of adding statically executable advice to AspectJ.