A mechanized Theory of Aspects

Over the past ten years, Aspect Orientation has emerged as a new paradigm in software engineering. The key feature promoted in this paradigm is the ability to modularize concerns - aspects - that by nature or implementation are orthogonal to the modular structure of the base application. To allow such a modularization, these aspect modules themselves are able to cut across the structure of the underlying application. This cutting across the structure goes beyond the mere referencing of remote data, allowing changes of the base application's control flow. Thus, Aspects offer the functionality of calling themselves instead of the intended target of an invocation. This altered invocation of the aspect is able to alter, extend or even replace parts of the original program. Being able to drastically alter the base application's structure comes at the price of a decrease in safety: aspects themselves do not fulfill the expectations held for classical modules and can even harm the modularization of the existing application. Basic concepts such as the locality of errors, type soundness and re-usability can thus be harmed by aspects. This thesis employs the method of rigorous language development on Aspect Orientation in order to show what classes of aspects maintain the safety of an application. Our rigorous approach entails the design of a family of aspect oriented core calculi, entirely mechanized in the interactive theorem prover Isabelle/HOL. The emphasis of the work is placed on two different fields. Fundamental questions of modularity, type soundness and subtyping form the first such field. Technical considerations such as binders, variable representation and code generation are the content of the other. Features of the Sigma-Asc calculi developed in this theses are a modular concept for aspects in an object oriented setting and several type systems building upon that foundation. These type systems enforce static type safety on aspects, while maintaining modularity and thus re-usability. This approach is also used to handle the variance issues encountered when combining aspects with depth subtyping. Furthermore, several classes of aspects are identified in the thesis, including a class of compositional aspects. In the field of language metatheory, the thesis contributes a comparative mechanization of the Sigma-Asc calculus introduced in this thesis, comparing the locally nameless and the de Bruijn variable representations.

Author dc:creator

• Sudhof, Henry

Advisor dc:contributor.advisor

• Jähnichen, Stefan

Licence dc:rights.uri

• https://creativecommons.org/licenses/by-sa/2.0/de

Language dc:language.iso

en, English

Identifier URI

urn:nbn:de:kobv:83-opus-26916
http://dx.doi.org/10.14279/depositonce-2501

OAI identifier oai:identifier

oai:depositonce.tu-berlin.de:11303/2798