Optimizing JML Features Compilation in Ajmlc
		  Using Aspect-Oriented Refactorings
				  by
	   Henrique Rebęlo, Ricardo Lima, Márcio Cornélio,
	   Gary T. Leavens, Alexandre Mota, César Oliveira
				   
			       Abstract

In previous work we presented a new JML compiler, ajmlc, which
generates aspects that enforce preconditions, postconditions, and
invariants. Although this compiler provides benefits of source-code
modularity and small bytecode size and running time, there is still a
need for optimization of bytecode size and running time. To do this
optimization while preserving the semantics of the resulting code, we
optimize using refactorings based on AspectJ programming laws. To this
end we present optimization refactorings and an empirical analysis
showing the resulting improvements. 

Keywords: ajmlc, runtime assertion checking, optimization, refactoring, 
semantics preservation, formal methods, formal interface
specification, programming by contract, JML language, Java 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 that will appear in the proceedings of
the XIII Brazilian Symposium on Programming Languages (SBLP 2009),
Gramado-RS, Brazil, August 19-21.