Babelsberg/RML

  • New programming language designs are often evaluated on concrete implementations. However, in order to draw conclusions about the language design from the evaluation of concrete programming languages, these implementations need to be verified against the formalism of the design. To that end, we also have to ensure that the design actually meets its stated goals. A useful tool for the latter has been to create an executable semantics from a formalism that can execute a test suite of examples. However, this mechanism so far did not allow to verify an implementation against the design. Babelsberg is a new design for a family of object-constraint languages. Recently, we have developed a formal semantics to clarify some issues in the design of those languages. Supplementing this work, we report here on how this formalism is turned into an executable operational semantics using the RML system. Furthermore, we show how we extended the executable semantics to create a framework that can generate test suites for the concrete BabelsbergNew programming language designs are often evaluated on concrete implementations. However, in order to draw conclusions about the language design from the evaluation of concrete programming languages, these implementations need to be verified against the formalism of the design. To that end, we also have to ensure that the design actually meets its stated goals. A useful tool for the latter has been to create an executable semantics from a formalism that can execute a test suite of examples. However, this mechanism so far did not allow to verify an implementation against the design. Babelsberg is a new design for a family of object-constraint languages. Recently, we have developed a formal semantics to clarify some issues in the design of those languages. Supplementing this work, we report here on how this formalism is turned into an executable operational semantics using the RML system. Furthermore, we show how we extended the executable semantics to create a framework that can generate test suites for the concrete Babelsberg implementations that provide traceability from the design to the language. Finally, we discuss how these test suites helped us find and correct mistakes in the Babelsberg implementation for JavaScript.show moreshow less
  • Neue Programmiersprachdesigns werden typischerweise anhand konkreter Implementierungen bewertet. Um jedoch Schlüsse aus den Erfahrungen mit einer konkreten Programmiersprache auf ein Sprachdesign ziehen zu können, muss die konkrete Sprache verifizierbar dem Design entsprechen. Zudem muss sichergestellt sein, dass das formale Design seine gesetzten Ziele auch erfüllt. Dabei haben sich ausführbare Semantiken als ein nützliches Werkzeug erwiesen, um letzteres sicherzustellen. Allerdings half dieses Werkzeug bisher nicht, auch die konkrete Implementierung gegen das Design zu verifizieren. Babelsberg ist ein neues Design für eine Familie von Objekt-Constraint Programmiersprachen, zu der wir eine formale Semantik entwickelt haben, die einige Details des Designs klarstellt. Ergänzend dazu berichten wir hier, wie dieser Formalismus in eine ausführbare Semantik mithilfe des RML Systems umgewandelt werden kann. Weiterhin zeigen wir, wie wir diese ausführbare Semantik um ein Rahmenwerk erweitert haben, mit dem sich programmatische Tests für dieNeue Programmiersprachdesigns werden typischerweise anhand konkreter Implementierungen bewertet. Um jedoch Schlüsse aus den Erfahrungen mit einer konkreten Programmiersprache auf ein Sprachdesign ziehen zu können, muss die konkrete Sprache verifizierbar dem Design entsprechen. Zudem muss sichergestellt sein, dass das formale Design seine gesetzten Ziele auch erfüllt. Dabei haben sich ausführbare Semantiken als ein nützliches Werkzeug erwiesen, um letzteres sicherzustellen. Allerdings half dieses Werkzeug bisher nicht, auch die konkrete Implementierung gegen das Design zu verifizieren. Babelsberg ist ein neues Design für eine Familie von Objekt-Constraint Programmiersprachen, zu der wir eine formale Semantik entwickelt haben, die einige Details des Designs klarstellt. Ergänzend dazu berichten wir hier, wie dieser Formalismus in eine ausführbare Semantik mithilfe des RML Systems umgewandelt werden kann. Weiterhin zeigen wir, wie wir diese ausführbare Semantik um ein Rahmenwerk erweitert haben, mit dem sich programmatische Tests für die konkreten Babelsberg Implementierungen erzeugen lassen, welche Rückverfolgbarkeit von der Sprachimplementierung zum Sprachdesign sicherstellen. Schlussendlich diskutieren wir, wie diese Tests uns erlaubten, Fehler in der Babelsberg Implementierung für JavaScript zu finden und zu beheben.show moreshow less

Download full text files

  • tbhpi103.pdfeng
    (3733KB)

    SHA-1:e5984b0419dfc4c9ce295ad1189eab1145801628

Export metadata

Additional Services

Share in Twitter Search Google Scholar Statistics
Metadaten
Author:Tim FelgentreffORCiDGND, Robert HirschfeldORCiDGND, Todd Millstein, Alan Borning
URN:urn:nbn:de:kobv:517-opus4-83826
ISBN:978-3-86956-348-0
ISSN:1613-5652 (print)
ISSN:2191-1665 (online)
Subtitle (English):executable semantics and language testing with RML
Series (Serial Number):Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam (103)
Publisher:Universitätsverlag Potsdam
Place of publication:Potsdam
Document Type:Monograph/Edited Volume
Language:English
Year of first Publication:2015
Year of Completion:2015
Publishing Institution:Universität Potsdam
Publishing Institution:Universitätsverlag Potsdam
Release Date:2016/06/28
Tag:Objekt-Constraint Programmierung; Sprachspezifikation; ausführbare Semantiken
executable semantics; language specification; object-constraint programming
Issue:103
Pagenumber:68
RVK - Regensburg Classification:ST 230
Organizational units:An-Institute / Hasso-Plattner-Institut für Digital Engineering gGmbH
Dewey Decimal Classification:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Publication Way:Universitätsverlag Potsdam
Licence (German):License LogoKeine Nutzungslizenz vergeben - es gilt das deutsche Urheberrecht
Notes extern:
In Printform erschienen im Universitätsverlag Potsdam:

Babelsberg/RML : executable semantics and language testing with RML / Tim Felgentreff, Robert Hirschfeld, Todd Millstein, Alan Borning. – Potsdam: Universitätsverlag Potsdam, 2016. – 66 S.
(Technische Berichte des Hasso-Plattner-Instituts für Softwaresystemtechnik an der Universität Potsdam ; 103)
ISSN (print) 1613-5652
ISSN (online) 2191-1665
ISBN 978-3-86956-348-0
--> bestellen