A generator for type checkers [Elektronische Ressource] / vorgelegt von Holger Gast

Holger Gast

Sujets

• Informatik

Informations

• Publié par: eberhard_karls_universitat_tubingen
• Publié le: 01 janvier 2005
• Nombre de lectures: 8
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

A Generator for Type Checkers
Dissertation
der Fakult at fur Informations- und Kognitionswissenschaften
der Eberhard-Karls-Universit at Tubingen
zur Erlangung des Grades eines
Doktors der Naturwissenschaften
(Dr. rer. nat.)
vorgelegt von
Dipl.-Inform. Holger Gast
aus Moers
Tubingen
2004Tag der mundlichen Quali kation: 8. Juni 2005
Dekan: Prof. Dr. Michael Diehl
1. Berichterstatter: Prof. Dr. Rudiger Loos
2. Berichter: Prof. Dr. Herbert Klaeren
3. Berichterstatter: Prof. Dr. David R. Musser
(Rensselaer Polytechnic Institute, NY, USA)Abstract
Compiler-compilers are tools that generate substitutes for hand-written compiler com-
ponents from high-level formal speci cations. Such tools exist for lexical, syntactic and
semantic analysis, optimizers and code generation. The established bene ts are reduced
development time and increased con dence in the correctness of the resulting software.
This thesis presents a generator for type checkers. Given a description of the type
system by typing rules, the generator yields a type checker that constructs proofs using
the typing rules. Unlike earlier approaches, we derive suitable notions of proof and typing
rule from an analysis of type systems and from corresponding constructs in mathematical
proof theory. The approach thus respects the structure and intention of the typing rules,
rather than expressing the rules in some pre-existing formalism.
Thegivenapplicationscomprisetypecheckersforimperative,object-orientedandfunc-
tional languages, including ML type inference. The typing rules for these checkers directly
represent those found in the literature. They naturally describe the typing of single lan-
guage constructs and they can be re-used in di erent checkers.
We use the generator to develop the languageSaga for generic programming. Generic
programming has become a standard approach to creating reusable and reliable software,
++particularly through the wide-spread use of the C Standard Template Library (STL).
++Existing C compilers cannot type-check generic algorithms before instances are gener-
ated,henceerrorsmanifestthemselvesonlywhenthealgorithmsareused. Sagaovercomes
this problem by a novel language design that enables generic algorithms as found in the
++C STL to be type-checked such that the correctness requirements stated in algorithm
interfacesareobeyedandinstantiationneverfails. Itthereforeturnstheaimsoftheearlier
proposal SuchThat into a concrete language design.Zuammenfassung
Compiler-compiler generieren aus formalen Spezi kationen Komponenten fur Compiler,
um dort handgeschriebenen Code ersetzen. Solche Generatoren existieren fur die lexika-
lische, syntaktische und semantische Anlayse, fur Optimierer und die Coderzeugung. Es
hat sich gezeigt, da die Entwicklungszeit abnimmt und gleichzeitig das Vertrauen in die
Korrektheit der Software steigt.
Die vorliegende Dissertation beschreibt einen Generator fur Typchecker. Er erzeugt
aus einer Spezi kation eines Typsystems, die in Form vom Typregeln gegeben ist, einen
ablau ahigenTypchecker,derTypherleitungenmitHilfedergegebenenRegelnkonstruiert.
Abweichendvonfruheren Vorschl agenwerdenpassendeDe nitionenfur Typherleitung und
Typregel durch Analyse existierender Typsysteme und der mathematischen Beweistheorie
gewonnen. Auf diese Weise re ektiert der Ansatz die Struktur und Intention der Typsys-
teme, anstatt die Typregeln in einem bereits vorhandenen Formalismus auszudruc ken.
Als Anwendungen werden Typchecker fur imperative, objekt-orientierte und funk-
tionale Sprachen, einschlie lich der ML Typinferenz, formalisiert. Die Typregeln dieser
Checker korrespondieren direkt mit den aus der Literatur bekannten. Da sie sich einzelnen
Sprachkonstrukten zuordnen lassen, k onnen sie in verschiedenen Checkern wiederverwen-
det werden.
Eine spezielle Anwendung ist die Sprache Saga fur die Generische Programmierung.
Die Generische Programmierung ist zu einem Standardansatz zur Erstellung verl a licher
und wiederverwendbarer Software geworden, insbesondere durch die weite Verbreitung der
++ ++C Standard Template Library (STL). Der C Compiler kann allerdings die gener-
ischen Algorithmen erst dann prufen, wenn konkrete Instanzen generiert werden. Fehler
in den Algorithmen manifestieren sich daher erst bei der Benutzung. Sagaostl dieses
Problem durch eine neues Sprachdesign, das es erlaubt, generische Algorithmen der STL
so zu ub erpruf en, da die deklarierten Korrektheitsbedingungen erfullt sind und die In-
stanzgenerierung nie fehlschl agt, wenn der Typchecker die Algorithmen akzeptiert. Damit
realisiert Saga die Ziele des fruheren Sprachvorschlags SuchThat in einem konkreten
Sprachdesign.Danksagungen
Zuallererst danke ich meinem Doktorvater, Prof. Dr. Rudig er Loos, herzlich fur die stetige
Unterstut zung meiner Arbeit. Durch die Mitarbeit in seiner Computeralgebra-Gruppe
w ahrend meines Studiums wurde ich erstmals auf die generische Programmierung und auf
die damit verbundenen Typfragen aufmerksam. Sein Interesse an meinen Ergebnissen und
Fragestellungenhatmichimmerwiederbe ugelt undvorneueHerausforderungengestellt.
Prof.Dr.HerbertKlaerengabmirdieM oglichkeit,dievorliegendeFassungalsMitglied
seinerArbeitsgruppeProgrammiersprachenundUbersetzerabzuschlie en. Diesererneuten
Uberarbeitung verdankt die Dissertation viel in Hinblick auf den direkten Ausdruck der
Typregeln und die e ziente Implementierung.
WeiterhindankeichmeinenKollegenamWilhelm-Schickard-Institut. Dr.RolandWeiss
++und Dr. Volker Simonis haben viel zu meinem Verstandnis der Sprache C beigetragen.
Dr. habil. Christoph Schwarzweller hat die Arbeiten an der Sprache Saga begleitet und
war stets o en fur Diskussionen ub er deren Typsystem. Dr. Carsten Sinz hat Teile von
Kapitel 2 durchgesehen.
Meiner Familie, insbesondere meinen Eltern Werner und Sibille Gast, danke ich herz-
lich fur den aufmunternden Ruc khalt und die F orderung meines fruhen Interesses an der
Programmierung. Ich danke Dorothea Flothow fur die Unterstutzung in der Endphase der
Uberarbeitung.Contents
1 Introduction 1
1.1 Statement of the Thesis . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.1.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
1.2 Designing a Type Check Generator . . . . . . . . . . . . . . . . . . . . . . 7
1.2.1 Preliminary Considerations . . . . . . . . . . . . . . . . . . . . . . 8
1.2.2 Comparison with Calculi for Logics . . . . . . . . . . . . . . . . . . 12
1.2.3 Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
2 Proofs 35
2.1 Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
2.1.1 Terms and Substitution . . . . . . . . . . . . . . . . . . . . . . . . 35
2.1.2 Uni ers and the Generalization Order . . . . . . . . . . . . . . . . . 37
2.1.3 Fixed Term Structure. . . . . . . . . . . . . . . . . . . . . . . . . . 39
2.2 Rules, Contexts and Judgments . . . . . . . . . . . . . . . . . . . . . . . . 39
2.2.1 Execution of Context Modi ers . . . . . . . . . . . . . . . . . . . . 42
2.3 Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
2.4 Derivation Steps . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
2.4.1 Instantiation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
2.4.2 Resolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
2.4.3 Adding a Pending Goal . . . . . . . . . . . . . . . . . . . . . . . . . 53
2.4.4 Deferring a Goal . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
2.4.5 Grafting Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
2.4.6 Outer Variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
2.5 Extensions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
2.5.1 Rule Expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
2.5.2 Lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60
3 Implementation 63
3.1 Tcg Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
3.1.1 Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
3.1.2 Parser Generator . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
3.1.3 Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
3.1.4 Deferred Goals and Proof Structure . . . . . . . . . . . . . . . . . . 69
3.1.5 External Presentations . . . . . . . . . . . . . . . . . . . . . . . . . 70
3.2 Translator . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70
i3.3 Interpreter . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
3.3.1 Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
3.3.2 Rules and Contexts . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
3.3.3 Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
3.3.4 Inference Steps . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
3.4 Search . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
3.5 GUI Inspector . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
3.6 Documentation Generator . . . . . . . . . . . . . . . . . . . . . . . . . . . 86
4 Applications 89
4.1 Exploring Tcg . . . . . . . . . . . . . . . . . . . . . . . . . . . .