AJML Tools: AspectJ-Based JML Tools

Motivation

Design by contract (DbC) is a method for developing software [1]. The key idea of DbC is that a class and its clients have a "contract" with each other. The client must guarantee certain conditions before calling a method defined by the class, and in return the class guarantees certain properties that will hold after the call. The use of such pre- and postconditions to specify software dates back to Hoare's 1969 work on formal verification [2]. In this context, the Java Modeling Language (JML) was conceived as a formal behavioral interface specification language (BISL) for Java that contains the essential notations used in the DbC methodology. JML tools such as JML compiler (jmlc) were designed, with several examples of their application. The main drawback of JML compiler [3] is that it cannot be used to other Java dialects such as Java ME. The instrumented bytecode generated by the standard JML compiler use Java reflection mechanism and data structures that are not supported by Java ME applications. In this context, we present a new JML compiler, called ajmlc [4, 5, 6], to support runtime assertion checking of Java Me applications annotated with JML. Besides that, in contrast with jmlc, there are other benefits of aspect-orientation adoption, such as better source and bytecode instrumentation size and better performance during runtime of applications.

The goals of the ajml tool are

• to check, compile, and run Java programs annotated with JML
• to genarate shorter source and bytecode instrumentation (compiler optimizations) than jmlc compiler
• to run programs compiled with ajmlc more faster than compiled with jmlc, and
• to support specification and verification during runtime of Java ME applications, which is not possible with standard jmlc compiler.

AJML Tool - Source Code - Old Releases - Credits

Installation

To install AJML tools, you should download the following Zip file, which constitutes the BINARY distribution, and unzip it in a directory of your preference.

1. AJML-1.1.zip

You'll need Java (or the Java runtime environment, jre) to run the checker and the assertion checking compiler (ajmlc). We've tested it with JDK version 1.5.0_09 and JRE 6.

Warning: the AJML tools do not work properly when using JDK 1.5 features, such as generics. You can use JDK 1.5 with the tools, but the annotated source code must contain features of JDK 1.4 or prior versions. (We are planning to fix this in the future.)

Getting Started

After you have successfully downloaded AJML tools, you are ready to start using it. Follow the following steps to get started with AJML.

1) Unpacking the zip file

Unpack the zip file in a folder which its path is

c:\JML

c:\JML\AJML-1.1

2) Running the tools

To run the ajml checker, from a command prompt, execute

	ajml file1.java file2.jml

To use the AspectJ runtime assertion checker compiler, use the ajmlc .bat script, for example:

	ajmlc file1.java

Note that the default weaver (AspectJ compiler) of ajmlc is the ajc, if you want to compile JML features using another weaver, use the following:

	ajmlc -aspectJCompiler "abc" file1.java

3) Running programs compiled with ajmlc

To run Java programs where some (or all) of the class files have been compiled with the AJML compiler (ajmlc), you will need to have the classes compiled in your Java "CLASSPATH". However, just having these classes in your "CLASSPATH" is not enough.

In addition to the compiled class files, you have to run a ajmlc-compiled program with AJML/bin/ajmlrt1.0.jar in your "CLASSPATH".

There is a .bat file for doing all of this easily. This script is called "ajmlrac". You would use it instead of the normal Java virtual machine ("java" command), as follows:

   ajmlrac my.package.name.ClassnameOfMain

where "ClassnameOfMain" is the class name of the class containing your program's main method, and "my.package.name" stands for the name of the package where "ClassnameOfMain" is found.

Getting Started using Eclipse

After you have successfully downloaded AJML tools, you are ready to start using it. Follow the following steps to get started with AJML within Eclipse platform.

Warning: this is not an Eclipse-based plugin for ajmlc. However, you can easily use ajmlc within Eclipse by using a custom Ant task, which is a part of the AJML release.

1) Demo Project

• Download the project Demo

• Create a simple Java project into Eclipse using the Demo project

2) Copying the AJML stuff

After you have successfully downloaded AJML tools, you should copy the jar files inside the "bin" folder and all AJML libraries contained into "ajml-lib" folder to a new folder named "lib-ajmlc1.0" within your Demo project. Afterwards, your project structure should look like as the figure below:

3) Compiling and Running the Demo program with AJML

To compile and run the Demo program using AJML, you need only to set some properties in "build.xml" file (you can see such a file in the project structure depicted above). In relation to this example, you need only to set the main class property, defined by the "main.class". Moreover, since this project does not have application specific libraries, you should comment the property "app.lib" and should also comment its reference in "classpath" (see details in the figure below).

In addition, you can see the AJML tasks in the ANT editor. First of all, open the ANT view in Eclipse as following:

   Window -> Show View -> Ant

Then in order to view the ant tasks provided by the "build.xml" file, you should drag and drop it in this view. Afterwards, you will see the main tasks as illustrated in figure below.

Now you are able to run AJML tools using ANT task. Click twice in the "ajmlc" task and then twice in the "ajmlrac" task. The results is illustrated in figure below

References

1. Bertrand Meyer. Applying "Design by Contract". Computer, v.25 n.10, p.40-51, October 1992.
2. C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969.
3. Yoonsik Cheon and Gary T. Leavens. A Runtime Assertion Checker for the Java Modeling Language (JML). In Hamid R. Arabnia and Youngsong Mun (eds.), International Conference on Software Engineering Research and Practice (SERP '02), Las Vegas, Nevada. CSREA Press, June 2002, pages 322-328.
4. Henrique Rebêlo, Ricardo Lima, Márcio Cornélio, Gary T. Leavens, Alexandre Mota, and César Oliveira. Optimizing JML Feature Compilation in Ajmlc using Aspect-Oriented Refactorings. Proceedings of the XIII Brazilian Symposium on Programming Languages (SBLP 2009), Gramado, Rio Grande do Sul, Brazil, August, 2009.
5. Henrique Rebêlo, Ricardo Lima, Márcio Cornélio, and Sérgio Soares. A JML compiler based on AspectJ. Proceeding of the 1st Internacional Conference on Software Testing, Verification, and Validation (ICST 2008), Lillehammer, Norway, April 9-11, 2008, pp. 541-544.
6. Henrique Rebêlo, Ricardo Lima, Márcio Cornélio, Sérgio Soares, and Leopoldo Ferreira. Implementing Java Modeling Language Contracts using AspectJ. Proceedings of the 23rd Annual ACM Symposium on Applied Computing (SAC 2008), Fortaleza, Ceará, Brazil, March 16-20, 2008, pp. 228-233.