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.

?
1
2
3
4
5
6
7
8
9
10
11
12
<!-- COMPILATIONS -->
 <!-- Note that these are the most common options used to run an AspectJML annotated Java program.
        - Also, these options include the advanced ones for AspectJML such as the crosscutting contract specifications
          with "crosscuttingcontractspecifications" option.
        - All these advanced ajmlc options are not enabled by default.
        - For more ajmlc options, please run the task above "ajmlc-help-options" and update the "ajmlc task" below to properly include them-->
 <!-- THE FUN HAS JUST BEGUN!! AspectJML team -->
 <target name="ajmlc" depends="clean,prepare" description="Ant task responsible for compiling Java files
                                              annotated with AspectJML using ajmlc compiler version ${AspectJML}">
     <ajmlc destdir="${dest.dir}" srcdir="${src.dir}" sourcepathref="sourcepath" classpathref="classpath" print="false" source="1.7" ajweaver="ajc" defaultnonnull="true" ...="">
     </ajmlc>
 </target>
As needed, you can configure the global properties in the build.xml file. The main properties are the following:
?
1
2
3
4
5
6
7
8
9
10
11
12
13
<!-- SYSTEM DEPENDENT VARIABLES        -   CHANGE FOR YOUR NEEDS  -->
    <property name="aspectjml.release.jar" value="aspectjml-lib/aspectjml-release1.7.0.jar"> </property>
    <property name="src.dir" value="src"> </property>
    <!-- From within Eclipse, you can put the generated bytecode directly at the "bin" folder and run the application direclty from Eclipse-->
    <!-- This tip is useful if you have several main classes and to avoid run one by one by changing the "main.class" property -->
    <property name="dest.dir" value="bin"></property>
    <!-- Target directory to print the instrumented source code (isc) as AspectJ aspects -->
    <property name="dest.dir.isc" value="isc"></property>
    <property name="crossref.dir" value="crossref"></property>
    <property name="main.class" value="my.package.name.ClassnameOfMain"></property>
    <property name="app.lib" value="lib"></property>
    <property name="aspectjml.lib" value="aspectjml-lib"></property>
    <!-- NOTE: 'aspectjml.lib' MUST INCLUDE ASPECTJ WEAVERS, AJC AND ABC -->
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.