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 - Installation

Downloading the Compiler

The AspectJML compiler can be obtained in the following forms:

  • BINARY distribution
  • SOURCE CODE distribution
Both are available here

Structure of AspectJML Distribution

The archive file contains the following folders.

  • bin: This folder contains the executable versions of the AspectJML compiler, including running scripts. The aspectjml-release1.7.0.jar is the complete version, which contains the classes needed to compile and run AspectJML.
  • aspectjml-lib: This folder contains all the libraries/dependencies needed to run the AspectJML compiler.
  • ant_tasks: This folder contains the build.xml files with ant tasks to run AspectJML from within Eclipse.

Requirements for Running AspectJML Compiler

  • Java Runtime Environment (JRE) 1.7. [please do not use Java Runtime Environment (JRE) 1.8 or greater due to changes in bytecode format]
  • If you need to use JRE 1.5 or 1.6, please email us and we'll be happy in exporting the desired AspectJML release with its bytecode compatible with JRE 1.5 or 1.6.
    This can also be done by anyone using the SOURCE CODE distribution.

Running the AspectJML Compiler

The AspectJML compiler can be used in two ways:

  • like javac from command-line
  • as a replacement builder for javac in the javac ant task; the tasks (within the build.xml file found in the bin directory) called ajmlc and ajmlrac are responsible for compiling and running programs, respectively.

Running the AspectJML Compiler from Within Ant

Use the following ajmlc ant task that can be used like the javac task to compile projects.
As needed, you can configure the global properties in the build.xml file. The main properties are the following:
For instance, the property src.dir, defines the place where the annotated classes are located. The dest.dir defines the folder where the bytecode is generated; the default value, as with eclipse, is bin, so that we can run the compiled annotated classes from within eclipse.