AspectJML crosscutting contract specifications for better modularity


          aspectjml is           aspectjml enables
 
  • a seamless aspect-oriented extension to the JML design by contract language
  • AspectJ compatible
  • Java platform compatible
  • easy to learn and use
  
  • clean modularization/specification of crosscutting contracts, such as preconditions and postconditions, while preserving documentation and modular reasoning
  • well-defined interfaces between the OO code and crosscutting contracts

AspectJML - Getting Started with AspectJML

The AspectJML Language

AspectJML extends JML with support for crosscutting contracts. It allows programmers to define additional constructs (in addition to those of JML) to
modularly specify pre- and postconditions and check them at certain well-defined points in the execution of a program. We call this the crosscutting
contract specification mechanism, or XCS for short.

XCS in AspectJML is based on a subset of AspectJ's constructs. However, since JML is a design by contract language tailored for plain Java, we need
special support to use the traditional AspectJ syntax. To simplify the adoption of AspectJML, the included AspectJ constructs are based on the alternative
@AspectJ syntax (which is part of the standard distribution of AspectJ).

The @AspectJ (often pronounced as "at AspectJ") syntax was conceived as a part of the merge of standard AspectJ with AspectWerkz. This merge enables
crosscutting concern implementation by using constructs based on the metadata annotation facility of Java 5. The main advantage of this syntactic style is
that one can compile a program using a plain Java compiler, allowing the modularized code using AspectJ to work better with conventional Java IDEs and
other tools that do not understand the traditional AspectJ syntax. In particular, this restriction applies to the JML common tools, including the JML compiler
on which ajmlc, the AspectJML compiler, is based.

In the following, we present how AspectJML supports crosscutting contract specification. The presentation is based on a running example.

XCS with Pointcuts-Specifications

The combination of pointcuts and specifications is AspectJML's way to modularize crosscutting contracts at source code level. Recall that a pointcut designator
enables one to select well-defined points in a program's execution, which are known as join points. Optionally, a pointcut can also include some of the values
in the execution context of intercepted join points. In AspectJML, we combine these AspectJ pointcuts with JML specifications.

The major difference, in relation to plain AspectJ, is that a specified pointcut is always processed when using our AspectJML compiler (ajmlc). In standard AspectJ,
a single pointcut declaration does not contribute to the execution flow of a program unless we define some AspectJ advice that uses such a pointcut. In AspectJML,
we do not need to define an advice to check a specification in a crosscutting fashion. Although it is possible to use advice declarations in AspectJML, we do not require them.
This makes AspectJML simpler and a programmer only needs to know AspectJ's pointcut language in addition to the main JML features.

Running Example

The code for this example is available here. The reader is also encouraged to consult our page on installing and running AspectJML compiler (ajmlc).
Also, the reader may refer to the main JML page for an overview of the main JML features. For an overview of AspectJ features, please refer to the AspectJ page.
Note that for AspectJML use, the reader may refer only to AspectJ's pointcut designators.

As an example, consider the canonical set of graphical shape classes, such as Point, Line, etc. Each element is part of the overall figure and implements the
Shape interface (for figure elements). The interface Shape is shown in the listing below. 

   interface Shape {}
The class Point is an example of a Shape. Points have an x and a y location and setter and getter methods setX, setY, getX, and getY. Points also have a method
moveBy, which updates the coordinates of point objects.

All five methods are specified with JML and illustrated below. 

  class Point implements Shape {
   int x, y; 
  
   //@ requires x >= 0;
   //@ ensures this.x == x;
   //@ signals_only \nothing;
   void setX(int x) {
    this.x = x;
   }
   
   //@ requires y >= 0;
   //@ ensures this.y == y;
   //@ signals_only \nothing;
   void setY(int y) {
    this.y = y;
   }
   
   //@ ensures \result >= 0;
   //@ signals_only \nothing;
   int getX() { return x; }
   
   //@ ensures \result >= 0;
   //@ signals_only \nothing;
   int getY() { return y; } 
   
   //@ requires dx >= 0 && dy >= 0;
   //@ ensures this.x == \old(this.x + dx)
   //@	     && this.y == \old(this.y + dy);
   //@ signals_only \nothing;
   void moveBy(int dx, int dy) {
    x += dx; y += dy;
   }
  }

Specifying crosscutting preconditions

Our first crosscutting contract scenario, regarding the above code, consists of two preconditions for any method, in Point with a name starting with set that returns void and takes one
argument of type int. That is, we cannot write preconditions constraining the input parameters on the methods setX and setY in Point, to be greater than or equal to zero, only once and
apply them to these or other methods with the same design constraints.

For this scenario, consider the JML annotated pointcut with the following precondition: 

  //@ requires xy >= 0;
  @Pointcut("execution(* Point.set*(int)) && args(xy)")
  void sets(int xy) {}
The pointcut sets matches all the executions of methods starting with "set" of class Point like setX and setY. As observed, this pointcut is exposing the intercepted method arguments of type
int. This is done in AspectJML by listing the formal parameters in the pointcut method. We bind the parameter names in the pointcut's expression (within the annotation @Pointcut) using the
argument-based pointcut args.

The main difference between this pointcut declaration and standard pointcut declarations in AspectJ is that we are adding one JML specification (using the requires clause). In this example the
JML says to check the declared precondition before the executions of intercepted methods.

Specifying crosscutting postconditions

We discuss now how to properly modularize crosscutting postconditions in AspectJML. JML supports two kinds of postconditions: normal and exceptional. Normal postconditions constrain methods
that return without throwing an exception. To illustrate AspectJML's design, we discuss two crosscutting scenarios from our running example.

For the first crosscutting scenario, we rely on JML normal postconditions. As such, the two normal postconditions of the methods getX and getY are the same. The JML ensures clause states that both
methods should return integer values greater than or equal to zero. In JML, we refer to the return values of a method using the special construct \result. The problem is that we cannot write a simple
and local quantified form of these postconditions and apply them to the constrained methods.

To handle this crosscutting scenario, we use the following specified pointcut in AspectJML: 

  //@ ensures ((int)\result) >= 0;
  @Pointcut("execution(int Point.get*())")
  void gets() {}
This pointcut constrains the executions of the getX and getY methods in Point to ensure that, after their executions, the returning integer values should be greater or equal to zero.

It is important to note that the JML \result expression, used within a pointcut declaration, should do a cast to the desired return type.

In relation to our second crosscutting scenarion (involving JML exceptional postconditions), we can observe that the specification //@ signals_only \nothing are written for all methods in Point to forbid
exceptions. There is no way to modularize such a JML contract in one place and apply it to all constrained methods. As a consequence, a programmer that adds 20 methods more in Point should explicitly
write the specification for all the added methods.

To modularize this second crosscutting postcondition scenario in AspectJML, we use the following JML annotated pointcut declaration: 

  //@ signals_only \nothing;
  @Pointcut("execution(* Point.*(..))")
  void pointMeths() {}
The above specification forbids the execution of any method in Point to throw an exception. If any intercepted method throws an exception (even a runtime exception), a JML exceptional postcondition error is thrown to signal the contract violation. In this pointcut, we do not expose any intercepted method's context. Hence, instead of writing //@ signals_only \nothing for all methods in Point, the pointcut pointMeths selects all the method executions in Point and adds the constraint "//@ signals_only \nothing" in a modular fashion.

Pointcut expressions without type signature patterns

In AspectJ, a pointcut expression can be defined without using a type signature pattern. A type signature pattern is a name (or part of a name) used to identify what type contains the join point. For example, the following AspectJ pointcut: 
 pointcut sets(): execution(* set*(int));
selects any method starting with "set" and has one argument of type int. In AspectJ, this pointcut matches any type in a system. Since we omit the type signature pattern, any type is candidate to expose the join points of interest. In AspectJ, although not required, we can also use a wildcard * to represent a type signature pattern that intercepts any type in the system (i.e., execution(* *.set*(int)). However AspectJML has a different semantics compared with AspectJ. For example, recall the previous pointcut method sets in AspectJML: 
  //@ requires xy >= 0;
  @Pointcut("execution(* Point.set*(int)) && args(xy)")
  void sets(int xy) {}
this pointcut method still selects the same methods starting with "set" and that has one argument of type int. The main difference is that even with the absence of the target type, AspectJML restricts the join points to the type (Point in this case) enclosing the pointcut declaration. AspectJML works in this manner to avoid the obliviousness problem to propagate to the JML specifications.

Specification of unrelated types

Another issue to consider is whether or not AspectJML can modularize inter-type ( Inter-types here are not the AspectJ feature that allows adding methods or fields with a static crosscutting mechanism. Instead, they are unrelated modules in a system; that is, types that are not related to each other but can present a common crosscutting contract structure.) crosscutting specifications. All the crosscutting contract specifications we discuss are related to one type (intra-type) or its subtypes. However, AspectJ can advise methods of different (unrelated) types in a system. This quantification property of AspectJ is quite useful but can also be problematic from the point of view of modular reasoning, since one needs to consider all the aspect declarations to understand the overall system behavior.

Instead of ruling this completely out, the design of AspectJML allows the specifier to use specifications that constrain unrelated inter-types, but in an explicit and limited manner.

As an example, recall our running example. We know that all the methods declared in Point are forbidden to throw exceptions (see the signals_only specification). Suppose now that the methods in Line class (which is a valid subtype of Shape) also have this constraint. Consider the following type declaration: 

 interface ExceptionSignalling {
  @InterfaceXCS
  class ExceptionSignallingXCS {
   //@ signals_only \nothing;
   @Pointcut("execution(* ExceptionSignalling+.*(..))")
   void allMeth() {}
  }
 }
This type declaration illustrates how we specify crosscutting contracts for interfaces. In @AspectJ, pointcuts are not allowed to be declared within interfaces. We overcome this problem by adding an inner class that represents the crosscutting contracts of the outer interface declaration. As a part of our strategy, the pointcut declared in the inner class refers only to the outer interface (see the reference in the pointcut predicate expression). Now any type that wants to forbid its method declarations to throw exceptions need only to implement the interface ExceptionSignallingConstraint (as shown below). Such an interface acts like a marker interface. This is important to avoid obliviousness and maintain modular reasoning. 
 class Point implements Shape, ExceptionSignallingXCS {...}
 
 class Line implements Shape, ExceptionSignallingXCS {...}

Note that the inner class is marked with the @InterfaceXCS annotation. This is to distinguish from any other inner class that could be also declared within our crosscutting contract interface. Without this mechanism, the AspectJML compiler will not be able to find the crosscutting contracts for the interface ExceptionSignalling.

Collected XCS examples

The resulting class Point with such modularized crosscutting contracts are shown below: 

  class Point implements Shape {
   int x, y; 
   
   // starting crosscutting contract specifications in AspectJML with pointcuts + specifications
   
   //@ requires xy >= 0;
   @Pointcut("execution(* Point.set*(int)) && args(xy)")
   void sets(int xy) {} 
   
   //@ signals_only \nothing;
   @Pointcut("execution(* Point.*(..))")
   void pointMeths() {} 
   
   //@ ensures ((int)\result) >= 0;
   @Pointcut("execution(int Point.get*())")
   void gets() {} 
   
   // ending of the crosscutting contract specifications in AspectJML
  
   //@ ensures this.x == x;
   void setX(int x) {
    this.x = x;
   }
   
   //@ ensures this.y == y;
   void setY(int y) {
    this.y = y;
   }
   
   int getX() { return x; }
   
   int getY() { return y; } 
      
   //@ requires dx >= 0 && dy >= 0;
   //@ ensures this.x == \old(this.x + dx)
   //@	     && this.y == \old(this.y + dy);
   void moveBy(int dx, int dy) {
    x += dx; y += dy;
   }
  }

For more details

For more details, please refer to our Modularity'14 paper at ACM DL.