Optimizing Generated Aspect-Oriented Assertion Checking Code
	  for JML Using Programming Laws: An Empirical Study

				  by
	   Henrique Rebęlo, Ricardo Lima, Gary T. Leavens, 
	   Márcio Cornélio, Alexandre Mota, César Oliveira
				   
			       Abstract

Aspect-oriented programming (AOP) enables the effective modularization of well-known crosscutting concerns. To take advantage of AOP, there are many techniques, including AOP laws, for a systematic refactoring of crosscutting concerns to aspects. However, there is also a need for supporting the systematic refactoring of AOP constructs. Existing techniques for aspect-oriented refactoring are too coarse-grained and make it too difficult to assure that the transformations preserve behavior and are indeed refactorings. This paper presents a catalogue of AOP laws towards a systematic refactoring of AOP constructs. As long as these laws are fine-grained, they make it easier to verify that the transformations they provide preserve behavior. Furthermore, as these laws can provide space and time optimization, we conduce an empirical study using four applications in optimized and non-optimized versions generated by ajmlc, a new JML compiler, presented in a previous work, which generates aspects that enforce JML contracts during runtime. We show that the AOP laws provide a significant improvement, regarding bytecode size and running time, in the aspect code generated by an optimized version of the ajmlc compiler.

Keywords: Aspect-oriented programming, refactoring, programming laws,
ajmlc, runtime assertion checking, optimization, refactoring, 
semantics preservation, laws of programming, formal methods, formal interface
specification, programming by contract, aspect-oriented programming,
JML language, Java language, AspectJ language.

2009 CR Categories:

D.2.1 [Software Engineering]
        Requirements/ Specifications --- languages, tools, JML;
D.2.2 [Software Engineering]
        Design Tools and Techniques --- 
                computer-aided software engineering (CASE);
D.2.4 [Software Engineering]
        Software/Program Verification --- Assertion checkers,
                class invariants, formal methods, programming by contract,
                reliability, tools, validation, JML;
D.2.5 [Software Engineering]
        Testing and Debugging --- Debugging aids, design,
                testing tools, theory;
F.3.1 [Logics and Meanings of Programs]
        Specifying and Verifying and Reasoning about Programs ---
                Assertions, invariants, pre- and post-conditions,
                specification techniques.

This is a preprint of a paper submitted for publication.