Dowody poprawności kompilatora

Szukam materiału instruktażowego, który obejmuje dowody poprawności kompilatora, najlepiej przy użyciu metod denotacyjnych, na poziomie początkującego studenta.

Alternatywnie, czy znasz kilka prostych przykładów kompilatora, których mógłbym zilustrować problemy? (Pierwszym przykładem, który przyszedł mi do głowy, był tłumacz z wyrażeń odrostkowych na wyrażenia postfiksowe. Ale nie pokazał niczego interesującego oprócz tego, jak wprowadzić indukcję w składni.)

Nie znam dobrych materiałów instruktażowych, ale są prace, które są wystarczająco podstawowe dla absolwenta (takiego jak ja). Pierwszy może być tym, czego szukasz (nacisk jest mój).

Proste dowody poprawności relacyjnej dla analiz statycznych i transformacji programu , Nick Benton. 2004.

Pokazujemy, w jaki sposób niektóre klasyczne analizy statyczne dla programów imperatywnych i optymalizujące je transformacje, które umożliwiają, mogą zostać wyrażone i okazały się prawidłowe przy użyciu elementarnych technik logicznych i denotacyjnych . Kluczowymi składnikami są interpretacja właściwości programu jako relacji, a nie predykatów, oraz uświadomienie sobie, że chociaż wiele analiz programu jest tradycyjnie formułowanych bardzo intensywnie, powiązane transformacje są w rzeczywistości możliwe dzięki bardziej liberalnym właściwościom ekstensywnym.

Te dokumenty mogą Cię również zainteresować. Pomogli mi bardzo!

1. Dowodzenie poprawności optymalizacji kompilatora przez Temporal Logic , David Lacey, Neil D. Jones, Eric Van Wyk, Carl Christian Frederiksen. Wydaje mi się, że w kontekście optymalizacji kompilatora jest więcej materiałów wykorzystujących bisimulację. Jeśli twoim celem są naprawdę techniki denotacyjne, prawdopodobnie możesz zakodować te dowody za pomocą charakterystyk bisimulacji.
2. Generowanie optymalizacji kompilatora na podstawie dowodów , Ross Tate, Michael Stepp i Sorin Lerner. Obejmuje teoretyczną kategorię formalizacji metody dowodowej.
3. Poprawne dostarczanie optymalizacji przy użyciu sparametryzowanej równoważności programu , Sudipta Kundu, Zachary Tatlock i Sorin Lerner. Idź tam, jeśli lubisz logiczne relacje.
4. Formalnie zweryfikowany kompilator zaplecza Xavier Leroy.

Będziesz musiał zmodernizować notację, ale poprawność kompilatora wyrażeń arytmetycznych McCarthy'ego i Paintera jest prosta i dobra, a także ma znaczenie historyczne (ponieważ według mojej najlepszej wiedzy jest to pierwszy artykuł na ten temat).

Certyfikowany kompilator zachowujący typ Adama Chlipali od Lambda Calculus do asemblera wydaje się być dobrym przykładem prostego dowodu poprawności kompilatora przy użyciu metod denotacyjnych, z dodatkową zaletą polegającą na tym, że został całkowicie sformalizowany w asystencie dowodu.

Graham Hutton ma mały przykład w swojej książce „Programowanie w Haskell”, która jest świetnym miejscem do rozpoczęcia.

Mam także kilka zmechanizowanych dowodów (różne logiki) kompilatora McCarthy-Painter w raporcie, który przygotowałem dla mojej doktoratu .

Być może nie najprostszy przykład, ale Xavier Leroy wykonał dużo pracy w tej dziedzinie, takich jak formalnie zweryfikowane kompilatora C . Poprowadził letnią prezentację szkolną przy użyciu małego imperatywnego języka IMP, który jest dostępnym wstępem do bardziej zaawansowanych prac.