AJML Tools: AspectJ-Based JML Tools

Henrique Rebęlo, Ricardo Lima, Gary T. Leavens, Márcio Cornélio, and Sérgio Soares


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.

AJML Tool - Source Code - Old Releases - Credits

Source Code Download

You should download the following Zip file, which constitutes the SOURCE distribution, and unzip it in a directory of your preference.

  1. AJML-3.2-src.zip



SVN Repository

In addition to getting the source from the zip file above, the source code for AJML2 can be found in the jmlspecs subversion repository

AJML2 source code is stored in the "AJML2/" using the traditional branches, tags and trunk folders (trunk contains the latest code).

The latest source can be viewed at https://jmlspecs.svn.sourceforge.net/svnroot/jmlspecs/AJML2/

AJML2 uses Ant as its build system. Running "ant" command at the top directory of AJML2 distribution should print the list of available build targets.



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.