Hi David and Pengcheng:

we need to push the issue how the class form program
defines a static checker a little bit further.

How does the following look?

-- Karl

The LoD checker in AspectJ for the class form 
provides the design for a static LoD checker 
in DJ.

\begin{quote}
 We have to collect the legal
 types on which a method call can happen before checking. We have
 {\em Pertype} and {\em Perscope} as abstract aspects, each of
 which defines an abstract pointcut
 (with the same name as the aspect!)
 which is used to collect preferred supplier types.
\end{quote}

We need to traverse from JavaProgram to MethodCall and 
maintain two sets of potential preferred supplier 
types: PertypePPS and PerscopePPS.

\begin{quote}
 The first situation is a global
 situation as defined by {\em Pertype}, in which some types are
 globally legal for methods of a type  no matter where the call
 site is. An example of that situation is the direct part
 situation, where the types of the instance variables of a class
 are always legal in any methods of the class. The second situation
 is the context situation as defined by {\em Perscope}, in which
 the types are only legal when the call sites are in the stack of a
 particular method execution. An example of that situation is the
 arguments situation, where the types of arguments are only legal
 for the scope of the method body.
 There are four concrete aspects  extending {\em Pertype} or {\em
 Perscope} aspect, which are corresponding to the four rules of LoD
 respectively.
\end{quote}

PertypePPS is updated whenever the traversal enters a new class.
We have a visitor method: 
void before(ClassDefinition host) that sets PertypePPS to
the set of the types of the instance variables of the class.

The collection of the PertypePPS information requires
a traversal through the ClassDefinition-object.

PerscopePPS is updated whenever the traversal enters a new method.
We have a visitor method:
void before(MethodDefinition host) that sets PertypePPS to
the set of the types that are
argument types or
return types of local method calls or
types whose constructor is called in the method.

The collection of the PerscopePPS information requires
a traversal through the MethodDefinition-object.

Issue:
There is a subtle difference between the class form
checker in AspectJ (per execution) and the DJ program: The AspectJ
program will reject 

// A a;
a.foo()
A a1 = new A();

while the DJ program will accept it because it will find
the constructor call.