Skip to main content
SpringerLink
Log in

Composing Safely — A Type System for Aspects

  • Conference paper
Software Composition (SC 2008)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 4954))

Included in the following conference series:

  • 351 Accesses

Abstract

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 errors. 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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abadi, M., Cardelli, L.: A Theory of Objects. Springer, Heidelberg (1996)

    MATH  Google Scholar 

  2. Abadi, M., Cardelli, L.: A Theory of Primitive Objects. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, Springer, Heidelberg (1994)

    Google Scholar 

  3. Avgustinov, P., et al.: Semantics of Static Pointcuts in Aspect. In: Principles of Programming Languages, POPL 2007, ACM Press, New York (2007)

    Google Scholar 

  4. Aydemir, B., Charguéraud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering Formal Metatheory. In: Principles of Programming Languages, POPL 2008, ACM Press, New York (2008)

    Google Scholar 

  5. Barendregt, H.P.: The Lambda Calculus, its Syntax and Semantics, 2nd edn. North-Holland, Amsterdam (1984)

    MATH  Google Scholar 

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

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

  9. Henrio, L., Kammüller, F.: A Mechanized Model of the Theory of Objects. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol. 4468, Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  10. Jähnichen, S., Kammüller, F.: Ascot: Formal, mechanical foundation of aspect-oriented and collaboration-based languages. DFG (2006), Web-page at, http://swt.cs.tu-berlin.de/~flokam/ascot/index.html

  11. Jagadeesan, R., Jeffrey, A., Riely, J.: Typed Parametric Polymorphism for Aspects. In [17], 267–296

    Google Scholar 

  12. Kammüller, F.: Interactive Theorem Proving in Software Engineering. Habilitationsschrift (habilitation thesis), Technische Universität Berlin (2006)

    Google Scholar 

  13. Kammüller, F., Vösgen, M.: Towards Type Safety of Aspect-Oriented Languages. In: Foundations of Aspect-Oriented Languages, FOAL 2006 (2006)

    Google Scholar 

  14. Ligatti, J., Walker, D., Zdancewic, S.: A type-theoretic interpretation of pointcuts and advice. In [17], pp. 240–266

    Google Scholar 

  15. Paulson, L.C.: Isabelle. LNCS, vol. 828. Springer, Heidelberg (1994)

    MATH  Google Scholar 

  16. Nipkow, T.: More Church Rosser Proofs. Journal of Automated Reasoning 26, 51–66 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  17. Science of Computer Programming: Special Issue on Foundations of Aspect-Oriented Programming. vol. 63(3), Elsevier (2006)

    Google Scholar 

  18. Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  19. Urban, C., Tasson, C.: Nominal Techniques in Isabelle/HOL. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, Springer, Heidelberg (2005)

    Google Scholar 

  20. Wright, A., Felleisen, M.: A Syntactic Approach to Type Soundness. Information and Computation 115, 38–94 (1994)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Insititut für Softwaretechnik und Theoretische Informatik, Technische Universität Berlin,  

    Florian Kammüller & Henry Sudhof

Authors
  1. Florian Kammüller
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Henry Sudhof
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Cesare Pautasso Éric Tanter

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kammüller, F., Sudhof, H. (2008). Composing Safely — A Type System for Aspects. In: Pautasso, C., Tanter, É. (eds) Software Composition. SC 2008. Lecture Notes in Computer Science, vol 4954. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78789-1_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-78789-1_18

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-78788-4

  • Online ISBN: 978-3-540-78789-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation