Composing safely: a type system for aspects

Article English OPEN
Kammueller, Florian ; Sudhof, Henry
  • Publisher: Springer
  • Subject:

In this paper we present an approach towards safe software composition based on aspect-orientation. Aspects enable the systematic addition of code into existing programs but often they also introduce er- rors. In order to provide safe aspects for software composition we address the verification of the aspect-oriented language paradigm. We construct a basic calculus for aspects with types and prove formally type safety. More precisely, this paper presents the following contributions (a) a fully formalized type system for the Theory of Objects including the proof of type safety, (b) a theory of aspects based on the Theory of Objects including a type system for aspects, and (c) the definition of a notion of type safety for aspects including its proof. The entire theory and proofs are carried out in the theorem prover Isabelle/HOL.
  • References (20)
    20 references, page 1 of 2

    1. M. Abadi and L. Cardelli. A Theory of Objects. Springer, 1996.

    2. M. Abadi and L. Cardelli. A Theory of Primitive Objects. Theoretical Aspects of Computing Software, TACS'94. LNCS 789, Springer, 1994.

    3. P. Avgustinov et al. Semantics of Static Pointcuts in Aspect, Principles of Programming Languages, POPL'07. ACM Press, 2007.

    4. B. Aydemir, A. Chargu´eraud, B. C. Pierce, R. Pollack and S. Weirich. Engineering Formal Metatheory, Principles of Programming Languages, POPL'08. ACM Press, 2008.

    5. H. P. Barendregt. The Lambda Calculus, its Syntax and Semantics. NorthHolland, 2nd edition, 1984.

    6. C. Clifton and G. Leavens. Minimao: Investigating the semantics of proceed. In Foundations of Aspect-Oriented Languages, FOAL'05, 2005.

    7. A. Ciaffaglione, L. Liquori, and M. Miculan. Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts. Journal of Automated Reasoning, 39:1-47, Springer, 2007.

    8. R. Filman and D. Friedman. Aspect-Oriented Programming is Quantification and Obliviousness. In Workshop on Advanced Separation of Concerns, OOPSLA 2000, Minneapolis, USA, October 2000.

    9. L. Henrio and F. Kammu¨ller. A Mechanized Model of the Theory of Objects. 9th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2007. LNCS 4468, Springer, 2007.

    10. S. J¨ahnichen and F. Kammu¨ller. Ascot: Formal, mechanical foundation of aspect-oriented and collaboration-based languages. Web-page at∼flokam/ascot/index.html. DFG, 2006.

  • Metrics
    No metrics available
Share - Bookmark