Please use this identifier to cite or link to this item: http://dx.doi.org/10.14279/depositonce-4736
Main Title: Type sound syntactic language extension
Translated Title: Typsichere syntaktische Spracherweiterung
Author(s): Lorenzen, Florian
Advisor(s): Pepper, Peter
Referee(s): Pepper, Peter
Mezini, Mira
Nestmann, Uwe
Granting Institution: Technische Universität Berlin, Fakultät IV - Elektrotechnik und Informatik
Type: Doctoral Thesis
Language: English
Language Code: en
Abstract: Syntaktische Erweiterungen von Programmiersprachen ermöglichen einen hohen Grad an Abstraktion, verringern die Notwendigkeit sich wiederholender oder gleichender Code-Fragmente, passen Sprachen an spezifische Anwendungsfelder an und sind ein essenzielles Werkzeug um die Software-Komplexität zu beherrschen und den Entwicklungsprozess produktiver zu gestalten. Syntaktische Spracherweiterungen werden üblicherweise durch eine Transformation (desugaring) zur Compile-Zeit in die Basissprache implementiert. Damit sie eine tragfähige Abstraktion bilden, darf der generierte Code keine Typfehler enthalten. Typfehler dieser Art bilden eine starke Einschränkung der Benutzbarkeit syntaktischer Erweiterungen: Sie werden relativ zum generierten Code gemeldet, was zu einer unvollständigen Abstraktion führt, sie sind häufig schwer zu finden und zu beheben und es ist oft unklar, ob die Definitions- oder die Anwendungsstelle einer Erweiterung fehlerhaft ist. In dieser Arbeit entwicklen wir das System und die Methode SoundX (Sound eXtensions) zur syntaktischen Spracherweiterung statisch typisierter Programmiersprachen. SoundX ist sprachunabhängig und lehnt sich an den Sugar*-Ansatz „Erweiterungen als Bibliotheken“ an. SoundX ermöglicht, einen syntaktisch erweiterbaren Dialekt aus der formalen Definition einer Basissprache abzuleiten. Die Definition einer Basissprache umfasst die kontextfreie Syntax und das Typsystem dieser Basissprache. Dabei wird das Typsystem durch induktiv definierte Relationen mittels Inferenzregeln spezifiziert. Die Definition einer Erweiterung besteht aus zusätzlichen Syntaxdeklarationen, Transformationsregeln, die die Erweiterung in die Basissprache übersetzen, sowie neuen Typregeln, die als Schnittstelle der Erweiterung fungieren. Erweiterungen können jede syntaktische Sorte der Basissprache erweitern, beispielsweise Terme, Typen oder Deklarationen. SoundX verwendet die Typregeln der Basissprache und der Erweiterungen zur Typanalyse bevor das Programm transformiert wird. Auf diese Art und Weise werden Typfehler relativ zum Originalprogramm gemeldet und die Transformation hat Typinformation für die Codegenerierung zur Verfügung. Dadurch werden Erweiterungen ermöglicht, die Typinferenz benötigen, und die Ausdrucksstärke wird im Vergleich zu rein syntaktischen Transformationen signifikant verbessert. Zur Nutzung von Typinformationen im Codegenerator bildet SoundX Typableitung statt reinen Ausdrücken der erweiterten Sprache in Typableitungen der Basissprache ab, wobei ein neuartiger ableitungsbasierter Algorithmus eingesetzt wird. SoundX garantiert, dass das Resultat der Transformation einer Erweiterung wohltypisiert ist. Zu diesem Zweck wird automatisch verifiziert, dass die Transformationsregeln und die Typregeln im Hinblick aufeinander korrekt sind. Wir beweisen ein Preservation-Theorem, das ausdrückt, dass die SoundX Verifikationsprozedur hinreichend ist, um sicherzustellen, dass eine gültige Typableitung in der erweiterten Sprache in eine gültige Typableitung der Basissprache übersetzt wird. Weiterhin charakterisieren wir mittels eines Progress-Theorems, unter welchen Umständen solch eine Ableitung als Resultat existiert. Nach dem „Erweiterungen als Bibliotheken“ Paradigma wird die Sichtbarkeit von Erweiterungen über das Modulsystem kontrolliert und Erweiterungen werden per Import aktiviert. Unabhängig voneinander definierte Erweiterungen werden beim Importieren komponiert und es ist möglich, dass eine Erweiterung von einer anderen Erweiterung inkrementell erweitert wird, indem erstere als Zielsprache genutzt wird. Die SoundX Verifikationsprozedur verifiziert Erweiterungen modular, so dass es nicht nötig ist, die Komposition von Erweiterungen erneut zu verifizieren. SoundX ist als ein Plugin für das Sugar* Framework implementiert, das eine Integration in die Eclipse-Entwicklungsumgebung bereitstellt. Die Implementierung enthält eine pragmatisch inspirierte aber fundierte Lösung zum praktisch relevanten Problem der Erzeugung frischer Namen während der Codegenerierung sowie eine Variation des Resolutionsalgorithmus, um einen Ableitungsbaum explizit aufzubauen. Zusätzlich enthält sie ein allgemeines und typsystemunabhängiges Verfahren, um Typfehler zu lokalisieren und zu melden, das in der Praxis angemessene und verständliche Fehlermeldungen liefert. Wir demonstrieren die Anwendbarkeit und die Ausdrucksstärke von SoundX durch mehrere Fallstudien, bei denen wir eine auf dem einfach typisierten Lambda-Kalkül basierende Basissprache nutzen.
Syntactic programming language extension provides a high level of abstraction, considerably reduces boilerplate code, adapts a programming language to a specific application area, and is an essential tool to manage complexity and to increase the productivity of the software development process. Syntactic language extensions are commonly implemented by rewriting or desugaring them into code of the base language at compile time. To form a sustainable abstraction, the desugaring of extended code must not introduce type errors in the generated code. These type errors are a serious threat to the usability of syntactic abstraction: they are reported in terms of the generated code leading to a leaky abstraction, they are often hard to find, and it is often unclear if the use site or the definition site of the extension is defective. In this thesis, we develop the language extension system and method SoundX (Sound eXtensions) for statically typed programming languages. SoundX is language independent and follows the “extensions as libraries” approach of Sugar*. It derives a syntactically extensible language dialect from a formal base language definition. A base language definition comprises the context-free syntax and the type system of the base language. The type system is specified by inductively defined judgements using inference rule schemata. Extensions consist of additional syntax, the desugaring into the base language, and new typing rules for the extended code that act as an interface of the extension. Extensions are free to add new phrases to all syntactic sorts of the base language like terms, types, or declarations. SoundX uses the typing rules of the base language and the extension to type check the extended program prior to desugaring. In this way, type errors are reported relative to the original sugared program and the desugaring can employ type information during the code generation. This allows the implementation of extensions that require type inference and significantly increases the expressiveness of SoundX compared to purely syntactical transformations. To process the type information in the code generator, SoundX maps typing derivations instead of plain expressions of the extended language to typing derivations of the base language using a novel derivation-centred desugaring procedure. SoundX guarantees that the desugaring of an extension results in well-typed code. To this end, it automatically verifies that the desugarings and the typing rules are sound with respect to each other. We formally prove that the SoundX verification procedure is sufficient to ensure that a valid derivation in the extended language is mapped to a valid derivation in the base language by establishing a Preservation theorem and characterise under which conditions such a resulting derivation exists using a Progress theorem. According to the “extensions as libraries” paradigm, extensions are scoped by the module system and activated by importing them. Independently defined extension are composed on import and it is possible to use one extension as the target of another extension enabling incremental extension. The SoundX verification procedure verifies an extension modularly and it is not necessary to re-verify the composition of extensions. SoundX is implemented as a plugin for the Sugar* framework providing an integration into the Eclipse IDE. The implementation contains a pragmatically inspired but principled solution to the practically relevant problem of fresh name generation during code generation and a variation of the resolution algorithm to obtain an explicit representation of a derivation tree. Moreover, it includes a general and type system independent procedure to locate and report type errors, which returns adequate and understandable error message in practice. We demonstrate the applicability and expressive- ness of SoundX by several case studies using a base language built on the Simply-Typed Lambda-Calculus.
URI: urn:nbn:de:kobv:83-opus4-72464
http://depositonce.tu-berlin.de/handle/11303/5033
http://dx.doi.org/10.14279/depositonce-4736
Exam Date: 25-Sep-2015
Issue Date: 16-Oct-2015
Date Available: 16-Oct-2015
DDC Class: 005 Computerprogrammierung, Programme, Daten
Subject(s): Erweiterbare Sprachen
Typsicherheit
automatische Verifikation
Programmtransformation
Typanalyse
Extensible languages
type soundness
automatic verification
program transformation
type checking
Creative Commons License: https://creativecommons.org/licenses/by/3.0/de/
Appears in Collections:Technische Universität Berlin » Fakultäten & Zentralinstitute » Fakultät 4 Elektrotechnik und Informatik » Institut für Softwaretechnik und Theoretische Informatik » Publications

Files in This Item:
File Description SizeFormat 
lorenzen_florian.pdf1.42 MBAdobe PDFThumbnail
View/Open


Items in DepositOnce are protected by copyright, with all rights reserved, unless otherwise indicated.