An Assume Guarantee Verification Methodology for Aspect-Oriented Programming

We propose a modular verification methodology for aspect oriented programs. Aspects are the new modularization units to encapsulate crosscutting concerns and have powerful features whose effects can drastically change software behavior. Having such an impact on behavior requires an automated verification support. In this work we introduce a technique that separately answers two questions: "does the aspect have the provisioned effect?" and "does the base program satisfy the assumptions of the aspect?" To answer these questions modularly, we propose using design contracts and state machines as aspect interfaces. An aspect interface both closes the environment of the aspect and specifies its assumptions on any base code. We show that our approach can be used in verifying AspectJ programs modularly and checking compatibility for aspect reuse.