JML and Aspects: The Benefits of Instrumenting JML Features with AspectJ

The Java Modeling Language (JML) is used to specify designs of Java classes and interfaces. To this end, JML has a rich set of features for specifying methods, including specification inheritance. Thus, the most fundamental motivation for employing JML is to improve functional software correctness of Java applications, and helps to reduce corrective maintenance effort of those applications. Previously, we presented a new JML compiler (ajmlc) that generates aspects (AspectJ) for contract enforcement. This paper describes the main reasons to instrument JML features with AspectJ, with particular emphasis on issues related to instrumentation code size — we also defined guidelines to use ajmlc that always generate compact instrumented code than the classical JML compiler (jmlc). In addition, we discuss the analogy between JML and AspectJ, and how the ajmlc also deals with Java ME applications, which is not possible with jmlc. Moreover, we implemented other JML features such as the new the new assertion semantics based on “strong validity ” presented elsewhere. The paper includes studies to compare the final code generated by ajmlc with the one produced by jmlc. Results indicate that the overhead in code size produced by our compiler is very small when using the proposed guidelines, which is essential for Java ME applications.