Compiler Korrektheitsbeweise

Ich bin auf der Suche nach Tutorial-Material, das Compiler-Korrektheitsnachweise, vorzugsweise unter Verwendung von Bezeichnungsmethoden, auf der Ebene eines Studienanfängers enthält.

Kennen Sie alternativ einige einfache Compiler-Beispiele, anhand derer ich die Probleme veranschaulichen könnte? (Das erste Beispiel, das mir einfiel, war ein Übersetzer von Infix- zu Postfix-Ausdrücken. Es zeigte jedoch nichts Interessantes, außer wie man die Syntax einführt.)

Ich kenne kein gutes Tutorial-Material, aber es gibt Papiere, die für einen Doktoranden (wie mich) ausreichend elementar sind. Das erste könnte das sein, wonach Sie suchen (der Schwerpunkt liegt bei mir).

Einfache relationale Korrektheitsnachweise für statische Analysen und Programmtransformationen , Nick Benton. 2004.

Wir zeigen, wie einige klassische statische Analysen für imperative Programme und die damit verbundenen optimierenden Transformationen mit elementaren logischen und denotationalen Techniken ausgedrückt und als richtig erwiesen werden können . Die Hauptzutaten sind eine Interpretation der Programmeigenschaften als Relationen und nicht als Prädikate und die Erkenntnis, dass viele Programmanalysen zwar traditionell in sehr intensiven Begriffen formuliert sind, die damit verbundenen Transformationen jedoch tatsächlich durch liberalere Erweiterungseigenschaften ermöglicht werden.

Diese Papiere könnten Sie auch interessieren. Sie haben mir sehr geholfen!

1. Beweisen der Korrektheit von Compiler-Optimierungen durch Temporal Logic , David Lacey, Neil D. Jones, Eric Van Wyk und Carl Christian Frederiksen. Ich hätte gedacht, dass es im Zusammenhang mit Compiler-Optimierungen mehr Material gibt, das Bisimulation verwendet. Wenn Ihr Ziel wirklich Konkretisierungstechniken sind, können Sie diese Beweise wahrscheinlich mithilfe von Charakterisierungen der Bisimulation kodieren.
2. Generierung von Compiler-Optimierungen aus Proofs , Ross Tate, Michael Stepp und Sorin Lerner. Beinhaltet eine kategorietheoretische Formalisierung ihrer Beweismethode.
3. Beweisen, dass Optimierungen mit parametrisierter Programmäquivalenz korrekt sind , Sudipta Kundu, Zachary Tatlock und Sorin Lerner. Gehen Sie dorthin, wenn Sie logische Beziehungen mögen.
4. Ein formal verifiziertes Compiler-Backend Xavier Leroy.

Sie müssen die Notation modernisieren, aber McCarthys und Malers Korrektheit eines Compilers für arithmetische Ausdrücke ist einfach und gut und auch von historischem Interesse (da es meines Wissens die erste Veröffentlichung zu diesem Thema ist).

Der von Adam Chlipala zertifizierte typerhaltende Compiler von Lambda Calculus bis Assembler scheint ein gutes Beispiel für einen einfachen Compiler-Korrektheitsnachweis unter Verwendung von Bezeichnungsmethoden zu sein, mit dem zusätzlichen Vorteil, dass er vollständig in einem Proof-Assistenten formalisiert wurde.

Graham Hutton hat ein kleines Beispiel in seinem Buch "Programming in Haskell", das ein guter Anfang ist.

Ich habe auch einige mechanisierte Beweise (verschiedene Logiken) des McCarthy-Painter-Compilers in einem Bericht, den ich für meine Promotion erstellt habe .

Vielleicht nicht das einfachste Beispiel, aber Xavier Leroy hat viel Arbeit in diesem Bereich geleistet, wie zum Beispiel einen formal verifizierten C-Compiler . Er hielt eine Summer School-Präsentation mit einer kleinen imperativen Sprache IMP, die eine leicht zugängliche Einführung in die fortgeschritteneren Arbeiten darstellt.