Preuves d'exactitude du compilateur

20

Je recherche du matériel didactique qui couvre les preuves d'exactitude du compilateur, de préférence en utilisant des méthodes de dénotation, au niveau d'un étudiant débutant.

Alternativement, connaissez-vous quelques exemples de compilateur simples que je pourrais utiliser pour illustrer les problèmes? (Le premier exemple qui m'est venu à l'esprit était un traducteur des expressions infixes vers postfixes. Mais il n'a pas montré quoi que ce soit d'intéressant autre que la façon de faire l'induction sur la syntaxe.)

Uday Reddy
la source

Réponses:

10

Je ne connais pas de bon matériel didactique, mais il existe des articles suffisamment élémentaires pour un étudiant diplômé (comme moi). Le premier pourrait être ce que vous recherchez (c'est moi qui souligne).

Preuves de correction relationnelle simples pour les analyses statiques et les transformations de programme , Nick Benton. 2004.

Nous montrons comment certaines analyses statiques classiques des programmes impératifs, et les transformations d'optimisation qu'elles permettent, peuvent être exprimées et prouvées correctes en utilisant des techniques élémentaires de logique et de dénotation . Les ingrédients clés sont une interprétation des propriétés du programme en tant que relations, plutôt que des prédicats, et une prise de conscience que bien que de nombreuses analyses de programme soient traditionnellement formulées en termes très intensionnels, les transformations associées sont en fait rendues possibles par des propriétés d'extension plus libérales.

Ces documents peuvent également vous intéresser. Ils m'ont beaucoup aidé!

  1. Prouver l'exactitude des optimisations du compilateur par Temporal Logic , David Lacey, Neil D. Jones, Eric Van Wyk, Carl Christian Frederiksen. J'aurais pensé qu'il y avait plus de matériel utilisant la bisimulation dans le contexte des optimisations du compilateur. Si votre objectif est vraiment des techniques de dénotation, vous pouvez probablement encoder ces preuves en utilisant des caractérisations de bisimulation.
  2. Génération d'optimisations du compilateur à partir de Proofs , Ross Tate, Michael Stepp et Sorin Lerner. Comprend une formalisation théorique de catégorie de leur méthode de preuve.
  3. Prouver des optimisations correctes en utilisant l'équivalence de programme paramétré , Sudipta Kundu, Zachary Tatlock et Sorin Lerner. Allez-y si vous aimez les relations logiques.
  4. Un back-end de compilateur officiellement vérifié Xavier Leroy.
Vijay D
la source
10

Vous devrez moderniser la notation, mais McCarthy et Painter's Correctness of a Compiler for Arithmetic Expressions est simple et bon, et présente également un intérêt historique (car, à ma connaissance, c'est le premier article sur le sujet).

Neel Krishnaswami
la source