Pruebas de corrección del compilador

Estoy buscando material tutorial que cubra las pruebas de corrección del compilador, preferiblemente utilizando métodos de denotación, al nivel de un estudiante graduado principiante.

Alternativamente, ¿conoce algunos ejemplos simples de compiladores que pueda usar para ilustrar los problemas? (El primer ejemplo que se me ocurrió fue un traductor de infix a expresiones de postfix. Pero no mostró nada interesante aparte de cómo hacer inducción en la sintaxis).

No conozco buen material de tutoría, pero hay documentos que son lo suficientemente elementales para un estudiante graduado (como yo). El primero podría ser lo que está buscando (el énfasis es mío).

Pruebas simples de corrección relacional para análisis estáticos y transformaciones de programas , Nick Benton. 2004

Mostramos cómo algunos análisis estáticos clásicos para programas imperativos, y las transformaciones de optimización que permiten, pueden expresarse y probarse correctas usando técnicas lógicas y denotacionales elementales . Los ingredientes clave son una interpretación de las propiedades del programa como relaciones, en lugar de predicados, y la constatación de que, aunque muchos análisis de programas se formulan tradicionalmente en términos muy intensivos, las transformaciones asociadas están realmente habilitadas por propiedades extensionales más liberales.

Estos documentos también pueden interesarle. ¡Me ayudaron mucho!

1. Probar la corrección de las optimizaciones del compilador por lógica temporal , David Lacey, Neil D. Jones, Eric Van Wyk, Carl Christian Frederiksen. Pensé que había más material usando bisimulación en el contexto de las optimizaciones del compilador. Si su objetivo es realmente técnicas denotacionales, probablemente pueda codificar estas pruebas usando caracterizaciones de bisimulación.
2. Generando optimizaciones del compilador a partir de pruebas , Ross Tate, Michael Stepp y Sorin Lerner. Incluye una formalización teórica de categoría de su método de prueba.
3. Probar optimizaciones correctas utilizando la equivalencia de programa parametrizada , Sudipta Kundu, Zachary Tatlock y Sorin Lerner. Ve allí si te gustan las relaciones lógicas.
4. Un compilador formalmente verificado Back-end Xavier Leroy.

Tendrá que modernizar la notación, pero McCarthy y Painter's Correctness of a Compiler for Arithmetic Expressions es simple y buena, y también de interés histórico (ya que, hasta donde sé, es el primer artículo sobre el tema).

El compilador certificado de preservación de tipos de Adam Chlipala, desde el cálculo de Lambda hasta el lenguaje ensamblador, parece ser un buen ejemplo de una prueba de corrección del compilador simple que utiliza métodos denotacionales, con la ventaja adicional de haber sido formalizado completamente en un asistente de prueba.

Graham Hutton tiene un pequeño ejemplo en su libro "Programación en Haskell", que es un excelente lugar para comenzar.

También tengo algunas pruebas mecanizadas (varias lógicas) del compilador McCarthy-Painter en un informe que hice para mi doctorado .

Quizás no sea el ejemplo más simple, pero Xavier Leroy ha hecho mucho trabajo en esta área, como un compilador de C verificado formalmente . Dio una presentación de la escuela de verano utilizando un pequeño IMP de lenguaje imperativo, que es una introducción accesible al trabajo más avanzado.