Formale, mechanisch unterstützte Fundierung aspektorientierter und kollaborationsbasierter Sprachen

• Applicant: Professor Dr.-Ing. Stefan Jähnichen
• Subject Area: Software Engineering and Programming Languages
• Term: from 2006 to 2010
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 24572631

• Final Report Year: 2010

Final Report Abstract

Im Rahmen des Projektes ASCOT haben wir den Kalkül ςAsc für Aspekte entwickelt. Die gesamte Entwicklung wurde vollständig in Isabelle/HOL mechanisiert und alle Aussagen uber die Sprache mit diesem System bewiesen, wodurch ein Höchstmaß an Konsistenz erreicht wird. Wir konnten die Kompositionalität des Aspekt-Weaving beweisen. Des weiteren konstruierten wir ein Typsystem mit Subtypen für Aspekte und konnten auf sehr modulare Art Typsicherheit beweisen. Die Formalisierung des Kalküls benutzt De-Bruijn- Indizes als Basis. Alternativ haben wir auch eine Formalisierung mit der Locally-Nameless-Technik erstellt. Wir haben mit Codegenerierung experimentiert. Schließlich konnte die Anwendbarkeit des Kalküls durch Analyse kritischer Beispiele aus realen aspektorientierten Programmen in AspectJ nachgewiesen werden.

Publications

• ASCOT – Formale, mechanisch unterstützte Fundierung aspektorientierter und kollaborationsbasierter Sprachen. Technische Universität München, 7. Juli, 2006
  F. Kammüller
  
• A Mechanized Framework for Aspects in Isabelle/HOL. ACM Workshop on Mechanizing Metatheory, Freiburg, 2007
  F. Kammüller and H. Sudhof
  
• A Mechanized Framework for Aspects in Isabelle/HOL. Workshop on Mechanizing Meta-Theory. Freiburg, 4. Oktober 2007
  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. Vol. 4468, LNCS, Springer, 2007
  L. Henrio and F. Kammüller
  
• Adapting Safely – HOL Theorem Proving applied to Aspect Orientation. United Nations University, International Institute for Software Technology, UNU-IIST, Macao, 27. Juli 2007
  F. Kammüller
  
• Exploring Object-Orientation with Interactive Theorem Proving. LORIA, Nancy, 19. März 2007
  F. Kammüller
  
• Exploring Object-Orientation with Interactive Theorem Proving. Université Grenoble, Laboratoire Informatique Grenoble LIG, 4. Mai, 2007
  F. Kammüller
  
• Formalizing Aspects for the ς-calculus in Isabelle/HOL. TR 2007-20, Technische Universität Berlin, 2007
  F. Kammüller and H. Sudhof
  
• A Mechanized Calculus for Aspect-oriented Programming. (Im Rahmen einer DAAD Summer-School). Universität Batna, Algerien, 1. April 2008
  F. Kammüller
  
• A Mechanized Calculus for Aspect-oriented Programming. Gesellschaft für Informatik, Beirat der Universitätsprofessoren, GIBU, Jahrestreffen, Schloss Dagstuhl, April 2008
  F. Kammüller
  
• Composing Safely – A Type System for Aspects. 7th International Symposium on Software Composition, SC’08. Satellite to ETAPS’08. Vol. 4954, LNCS, Springer, 2008
  F. Kammüller and H. Sudhof
  
• Composing Safely – A Type System for Aspects. Software Composition. Budapest, April 2008
  H. Sudhof
  
• Compositionality of Aspect Weaving. Autonomous Systems – Self-Organisation, Management, and Control. B. Mahr, H. Sheng (Eds.), Springer, 2008
  F. Kammüller and H. Sudhof
  
• Compositionality of Aspect Weaving. Autonomous Systems – Self-Organisation, Management, and Control. JiaoTong Universität, Shanghai, 6. Oktober, 2008
  F. Kammüller
  
• Un Calcul Mécanisé pour la Programmation Orientée Aspect. Université Besanon, 5. Mai, 2008
  F. Kammüller
  
• A Mechanized Theory of Aspects. Theorem Proving in Higher Order Logics. 22nd International Conference, Emerging Trends. Munich, August, 2009
  F. Kammüller and H. Sudhof
  
• A Mechanized Theory of Aspects. TPHOLs 2009, April 2009
  H. Sudhof
  
• Ascot Webseite, 2010