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
AspectJML: Modular Specification and Runtime Checking for Crosscutting Contracts by Henrique Rebelo, Gary T. Leavens, Mehdi Bagherzadeh, Hridesh Rajan, Ricardo Lima, Daniel M. Zimmerman, Marcio Cornelio, and Thomas Thum Abstract Aspect-oriented programming (AOP) is a popular technique for modularizing crosscutting concerns. In this context, researchers have found that the realization of design by contract (DbC) is crosscutting and fares better when modularized by AOP. However, previous efforts aimed at supporting crosscutting contracts modularly actually compromised the main DbC principles. For example, in AspectJ-style, reasoning about the correctness of a method call may require a whole-program analysis to determine what advice applies and what that advice does relative to DbC implementation and checking. Also, when contracts are separated from classes a programmer may not know about them and may break them inadvertently. In this paper we solve these problems with AspectJML, a new specification language that supports crosscutting contracts for Java code. We also show how AspectJML supports the main DbC principles of modular reasoning and contracts as documentation. Keywords: Design by contract, aspect-oriented programming, crosscutting contracts, JML, AspectJ, AspectJML. CR Categories: D.2.4 Software/Program Verification -- Programming by contract, Assertion Checkers; F.3.1 Specifying and Verifying and Reasoning about Programs -- Assertions, Invariant, Pre- and postconditions, Specification techniques.