Code generation from specifications in higher-order logic [Elektronische Ressource] / Florian Haftmann

Sujets

• Wissenschaft

Informations

• Publié par: technische_universitat_munchen
• Publié le: 01 janvier 2009
• Nombre de lectures: 31
• Langue: Deutsch
• Poids de l'ouvrage: 1 Mo

Extrait

Lehrstuhl fur Software & Systems Engineering
Institut fur Informatik
Technische Universitat Munchen
Code Generation
from Speci cations in Higher-Order Logic
Florian Haftmann
Vollstandiger Abdruck der von der Fakultat fur Informatik der Technischen Univer-
sitat Munc hen zur Erlangung des akademischen Grades eines
Doktors der Naturwissenschaften (Dr. rer. nat.)
genehmigten Dissertation.
Vorsitzender: Univ.-Prof. Dr. Florian Matthes
Prufer der Dissertation:
1. Univ.-Prof. Tobias Nipkow, Ph.D.
2. Dr. Helmut Seidl
Die Dissertation wurde am 27. Mai 2009 bei der Technischen Universitat Munchen
eingereicht und durch die Fakultat fur Informatik am 9. November 2009 angenom-
men.Zusammenfassung
Ein sehr rigoroser Ansatz zur Vermeidung fehlerhaft implementierter Software ist for-
male Veri kation: sowohl Verhaltensbeschreibung (abstrakte Spezi kation) als auch
Implementierung (ausfuhrbare Spezi kation) werden in einem geeigneten logischen
Kalkul beschrieben, und es wird gezeigt, dass beide sich gleich verhalten. Schon auf-
grund der zahlreichen technischen Details liegt es nahe, das Uberprufen der einzelnen
Beweisschritte innerhalb eines Beweisassistenten vorzunehmen. Dieser mechanische
Ansatz ermoglic ht es auch, in gewissen Fallen eine ausfuhrbare Spezi kation auto-
matisch in ein Programm in einer geeigneten Programmiersprache zu ub erfuhren.
Dieses etablierte Verfahren ist als Code-Generierung bekannt.
Ziel dieser Arbeit ist die Darstellung eines Codegenerator-Frameworks fur den
interaktiven Theorembeweiser Isabelle/HOL, einer Implementierung hoherstu ger
Logik. Gegenuber existierenden Ansatzen weist das Framework zwei substantielle
Neuerungen auf: ein sehr allgemeines, aber leichtgewichtiges Konzept fur Daten-
typabstraktion und die Unterstutzung von Isabelle-Typklassen im Sinne von Has-
kell-Typklassen. Konzeptionell moglich ist Generierung von Code fur funktionale
Sprachen mit Pattern Matching; konkrete Instantiierungen des Frameworks liegen
vor fur die Zielsprachen SML, OCaml und Haskell.
Die praktische Verwendbarkeit des Codegenerator-Frameworks wird mit exempla-
rischen Anwendungen demonstriert.Abstract
A very rigorous weapon against implementation errors in software systems is formal
veri cation: both the desired behaviour (abstract speci cation) and the implemen-
tation (executable speci cation) are formalised in a suitable logical calculus, and
the equivalence of both is proved. The numerous technical details involved in such
a procedure suggest to let a proof assistant check all proof steps. This mechani-
cal approach in certain cases enables an automatic translation from an executable
speci cation to a program in a suitable programming language: code generation.
The aim of this thesis is to present a code generator framework for the interactive
proof assistant Isabelle/HOL, an implementation of higher-order logic. The frame-
work includes two substantial novelties: a general but lightweight concept for data-
type abstraction and support for Isabelle type classes in the manner of Haskell type
classes. Code can be generated for functional programming languages supporting
pattern matching; concrete instances for SML, OCaml and Haskell are presented.
The practical usability of the code generator framework is demonstrated with
example applications.In memoriam Werner Krehbiel (1941{2004)Acknowledgements
The accomplishment of this thesis has been a ful lling and absorbing task in all
its facets: acquisition of knowledge, system development, elaboration. This would
not have been possible without the constant support and feedback from the Isabelle
group in Munich, whose (former and current) members I am deeply indebted to:
Tobias Nipkow gave me the opportunity to work in his research group and super-
vised this thesis; Alexander Krauss was a travel mate on my journeys in both the
gurative and literal sense; Stefan Berghofer and Makarius Wenzel supported and
helped me patiently in my starting time; further Clemens Ballarin, Gertrud Bauer,
Jasmin Blanchette, Sascha B ohme, Lukas Bulwahn, Amine Chaieb, Johannes H olzl,
Julien Narboux, Steven Obua, Norbert Schirmer, Christian Urban, Tjark Weber
and Martin Wildmoser | may future generations of PhD students enjoy the same
enlightenment, pleasure and friendly working atmosphere with and around Isabelle
as I had the opportunity to experience.
Further thanks I owe to Helmut Seidl for acting as referee.
Among the many people involved with Isabelle whose centre of life is not in Munich
I would like to mention Larry Paulson, John Matthews, Brian Hu man and Gerwin
Klein, who gave important inspiration and feedback for my work.
Preliminary parts of this thesis have been read and commented by Alexander Krauss,
Sascha B ohme, Makarius Wenzel and Jasmin Blanchette, whom I would like to thank
in particular for his language expertise | remaining de ciencies still fall under my
responsibility.
This research was nancially supported by the DFG project NI 491/10-1.