Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
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.