One approach towards adaptivity is aspect-orientation. Aspects enable the systematic addition of code into existing programs. In order to provide safe and at the same time flexible aspects for such adaptive systems we address the verification of the aspect-oriented language paradigm. This paper first gives an overview of our aspect calculus and summarizes previous results. Then we present a new composi-tionality lemma prerequisite for so-called run-time weaving. The entire theory and proofs are carried out in the theorem prover Isabelle/HOL.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
M. Abadi and L. Cardelli. A Theory of Objects. Springer, New York, 1996.
H. P. Barendregt. The Lambda Calculus, its Syntax and Semantics. North-Holland, 1984.
L. Henrio and F. Kamm üller. A Mechanized Model of the Theory of Objects. 9th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS’07. LNCS 4468, Springer, 2007.
S. J ähnichen and F. Kamm üller. Ascot: Formal, Mechanical Foundation of Aspect-Oriented and Collaboration-Based Languages. Web-page at http://swt.cs.tu-berlin.de/∼ flokam/ascot/index.html Project with the German Research Foundation (DFG), 2006.
F. Kamm üller. Exploring New OO-Paradigms in HOL: Aspects and Collaborations. Theorem Proving for Higher Order Logics, TPHOLs’05, Emerging trends. Technical Report PRG-RR05-02, Oxford University, 2005.
F. Kamm üller. Interactive Theorem Proving in Software Engineering. Habilitationsschrift (habilitation thesis), Technische Universit ät Berlin, 2006.
F. Kamm üller and H. Sudhof. A Mechanized Framework for Aspects in Isabelle/HOL. 2nd ACM SIGPLAN Workshop on Mechanizing Metatheory, 2007.
F. Kamm üller and H. Sudhof. Composing Safely - A Type System for Aspects. 7th International Symposium on Software Composition, SC’08. Satellite to ETAPS’08. LNCS 4954, Springer 2008.
F. Kamm üller and M. V ösgen. Towards Type Safety of Aspect-Oriented Languages. In Foundations of Aspect-Oriented Languages, AOSD’06, 2006.
J. Ligatti, D. Walker, and S. Zdancewic. A type-theoretic interpretation of pointcuts and advice. Science of Computer Programming: Special Issue on Foundations of Aspect-Oriented Programming. Springer 2006.
T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, LNCS 2283, Springer 2002.
The POPLmark challenge. http://alliance.seas.upenn.edu/∼plclub/cgi-bin/ poplmark. July 2007.
C. Urban et al. Nominal Methods Group. Project funded by the German Research Foundation (DFG) within the Emmy-Noether Programme, 2006.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer Science + Business Media B.V
About this paper
Cite this paper
Kammüller, F., Sudhof, H. (2008). Compositionality of Aspect Weaving. In: Mahr, B., Huanye, S. (eds) Autonomous Systems – Self-Organization, Management, and Control. Springer, Dordrecht. https://doi.org/10.1007/978-1-4020-8889-6_10
Download citation
DOI: https://doi.org/10.1007/978-1-4020-8889-6_10
Publisher Name: Springer, Dordrecht
Print ISBN: 978-1-4020-8888-9
Online ISBN: 978-1-4020-8889-6
eBook Packages: EngineeringEngineering (R0)