A mechanized Theory of Aspects
| dc.contributor.advisor | Jähnichen, Stefan | en |
| dc.contributor.author | Sudhof, Henry | en |
| dc.contributor.grantor | Technische Universität Berlin, Fakultät IV - Elektrotechnik und Informatik | en |
| dc.date.accepted | 2010-05-28 | |
| dc.date.accessioned | 2015-11-20T19:38:35Z | |
| dc.date.available | 2010-06-25T12:00:00Z | |
| dc.date.issued | 2010-06-25 | |
| dc.date.submitted | 2010-06-25 | |
| dc.description.abstract | 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. | en |
| dc.description.abstract | In den vergangenen zehn Jahren hat sich Aspektorientierung als ein neues Paradigma in der Softwaretechnik etabliert. Dieses Paradigma erlaubt die Modularisierung von Funktionalitäten, die orthogonal zur eigentlichen Modulstruktur eines Programms liegen. Um dies zu ermöglichen, sind solche Aspektmodule selbst nicht an die Modulstruktur gebunden, sondern in der Lage diese zu durchbrechen. Dieses Durchbrechen geht über Referenzieren bestehender Strukturen hinaus, vielmehr verändern Aspekte den Kontrollfluss der ursprünglichen Anwendung und verursachen so ihre eigene Ausführung. Dieser invertierte Kontrollflusses bietet somit die Möglichkeit, Teile des ursprünglichen Programms zu ergänzen, zu entfernen oder zu ersetzen. Diese Fähigkeit geht mit einem Sicherheitsverlust einher: Aspekte erfüllen oft nicht die Erwartungen an Module und können die Modularisierung der eigentlichen Basisanwendung sogar stören. Grundsätzliche Anforderungen an Module wie Fehlerlokalität, Typsicherheit oder Wiederverwendbarkeit sind somit für Aspekte beziehungsweise mit ihnen nicht unbedingt erfüllt. Die vorliegende Arbeit behandelt die Thematik rigoros, indem eine Familie von aspektorientierten Kalkülen vollständig in dem interaktiven Theorembeweiser Isabelle/HOL entwickelt wird. Dazu werden zunächst die Grundlagen mechanisierter Sprachtheorie eingeführt und bestehende Ansatze zur formalen Behandlung von Aspekten verglichen. Der darauf aufbauende wissenschaftliche Beitrag gliedert sich in zwei Bereiche: Den der formalen Behandlung der Aspektorientierung und den der mechanisierten Sprachtheorie. Im ersten Feld besteht der Beitrag dieser Arbeit zunächst in der Entwicklung eines aspektorientierten Kernkalküls auf Grundlage des Sigma Kalküls. Wichtige Kerneigenschaften des Kalküls werden bewiesen und es wird ein Kompositionalitätsbegriff für Aspekte entwickelt. Ferner ist die statische Analyse von Aspekten mittels Typsystemen Gegenstand der Arbeit, zunächst mittels eines einfachen modularen Typsystems, dann in iterativen Schritten um Subtyping und Varianz erweitert. Jedes vorgestellte Typsystem zur Typisierung von Aspekten umfasst einen kompletten Beweis der Typsicherheit. Ergebnisse des Kalküls werden im Wege einer Codegenerierung und einer Szenarienanalyse auf die Ebene der Anwendbarkeit übertragen. Darauf aufbauend, erfolgt die Entwicklung einer Kategorisierung von Aspekten aufgrund ihrer Sicherheitseigenschaften. Auf dem Gebiet der mechanisierten Sprachentwicklung stellt diese Arbeit ein objekt- und aspektorientiertes Kalkül vor, das vollständig in dem interaktiven Theorembeweiser Isabelle/HOL realisiert wurde. Auf Basis dieses Kalküls wurden zudem zwei verschiedene Variablenrepräsentationen erprobt und gegenübergestellt. Dieser direkte Vergleich bietet einen weiteren Beitrag für die Mechanisierung von Sprachen. | de |
| dc.identifier.uri | urn:nbn:de:kobv:83-opus-26916 | |
| dc.identifier.uri | https://depositonce.tu-berlin.de/handle/11303/2798 | |
| dc.identifier.uri | http://dx.doi.org/10.14279/depositonce-2501 | |
| dc.language | English | en |
| dc.language.iso | en | en |
| dc.rights.uri | https://creativecommons.org/licenses/by-sa/2.0/de | en |
| dc.subject.ddc | 004 Datenverarbeitung; Informatik | en |
| dc.subject.other | Aspektorientierung | de |
| dc.subject.other | Isabelle/HOL | de |
| dc.subject.other | Sigma-Kalkül | de |
| dc.subject.other | Theorembeweiser | de |
| dc.subject.other | Typen | de |
| dc.subject.other | Aspect orientation | en |
| dc.subject.other | Isabelle/HOL | en |
| dc.subject.other | Sigma calculus | en |
| dc.subject.other | Theorem provers | en |
| dc.subject.other | Types | en |
| dc.title | A mechanized Theory of Aspects | en |
| dc.title.translated | Eine mechanisierte Aspektheorie | de |
| dc.type | Doctoral Thesis | en |
| dc.type.version | publishedVersion | en |
| tub.accessrights.dnb | free | * |
| tub.affiliation | Fak. 4 Elektrotechnik und Informatik::Inst. Softwaretechnik und Theoretische Informatik | de |
| tub.affiliation.faculty | Fak. 4 Elektrotechnik und Informatik | de |
| tub.affiliation.institute | Inst. Softwaretechnik und Theoretische Informatik | de |
| tub.identifier.opus3 | 2691 | |
| tub.identifier.opus4 | 2560 | |
| tub.publisher.universityorinstitution | Technische Universität Berlin | en |
Files
Original bundle
1 - 1 of 1