Diese Dissertation wird die Art der Verbindung zwischen statischen Typsystemen und Programmverifikation untersuchen. Es wird also der Frage nachgegangen, warum es keine verifizierbaren, dynamisch getypten Programmiersprachen gibt. Wir werden aufzeigen, dass die häufige Kombination aus statischem Typsystem und Programverifikation nicht auf Notwendigkeit beruht, sondern lediglich auf Bequemlichkeit. In diesem Sinne werden wir eine dynamisch getypte Programmiersprache und eine Programmlogik definieren, deren Korrektheit und (relative) Vollständigkeit beweisen, einen Ansatz entwickeln, den zusätzlichen Verifikationsaufwand bei dynamisch getypten Programmen zu reduzieren, und zu guter Letzt die statische und dynamische Typisierung auf eine neuartige Art kombinieren, die es ermöglicht, die Typ-Sicherheit von dynamisch getyptem Programmcode zu garantieren, ohne ihn in statisch getypten umschreiben zu müssen und dabei sowohl Soft- als auch Gradual-Typing generalisiert. <dt.>
This thesis investigates the connection between static typing and program verification, or - phrased from the opposite direction - seeks to answer the question “why are there no verifiable, dynamically typed programming languages?”. We will demonstrate in this thesis that although common, the combination of static typing and program verification is not based on neccessity, but on convenience. To that end, we will define a dynamically typed programming language along with a program logic that we demonstrate to be both sound and (relative) complete, develop an approach to mitigate the overhead experienced during verification of dynamically typed programs, and finally combine static- and dynamic typing in a novel way, which enables deriving type safety guarantees for dynamically typed code without rewriting it into statically typed code and thereby generalizes both soft- and gradual typing. <engl.>
Proceedings of the young researchers conference "frontiers of formal methods" Aachen : RWTH Aachen, Dept. of Computer Science, 2015 (2015), Seite 87-92 Online-Ressource (279 Seiten, 14,32 MB)
