Aspect-oriented programming systems provide powerful mechanisms for separating concerns in source code, but understanding how these concerns interact can be challenging. In this talk, I will provide a brief overview before motivating the modular reasoning problem:  many aspect-oriented programming constructs can violate encapsulation, making it difficult to reason about a module's correctness in isolation.

Our proposal for addressing this problem is Open Modules, a mechanism for enforcing a strong form of encapsulation while supporting much of the extensibility provided by languages like AspectJ. Open Modules provide extensibility by allowing clients to advise the interface of a module, but enforce encapsulation by protecting internal function calls made within a module. A module can expose semantically important internal events to clients through pointcuts in its interface. The module's implementation can change without affecting client advice as long as the semantics of the pointcuts in its interface are preserved.

Using TinyAspect, a formally defined language modeling core aspect-oriented programming constructs, we define the semantics of Open Modules and prove type soundness. We use a notion of bisimulation to show that Open Modules enforce Reynold's abstraction theorem, a strong encapsulation property.