Verified normalization of the Lustre language
Normalisation vérifiée du langage Lustre
Résumé
Lustre is a synchronous dataflow language designed for programming embedded systems. In the Vélus project, we use Coq to develop and formalize a compiler that accepts a normalized form of the language and produces imperative code. While this restricted form is suitable for code generated from a user interface based on block diagrams, we wanted to allow programmers to use the
complete language.
In this article, we present the normalization pass that transforms the complete language into the normalized one. This transformation is divided into three steps so as to simplify the correctness proofs. To show that the semantics is preserved, it is necessary to prove that the three steps preserve certain static and dynamic properties of the language. In particular, the relation between the clock types and the dynamic semantic must be established.
Lustre est un langage synchrone à flots de données conçu pour programmer des systèmes embarqués. Dans le cadre du projet Vélus, nous avons développé et formalisé dans Coq un compilateur qui accepte une forme normalisée du langage et la compile vers du code impératif. Si cette forme réduite prend en charge un code généré depuis une interface utilisateur basée sur les schémas-blocs, nous voulons offrir au programmeur la possibilité de manipuler le langage complet.
Dans cet article nous présentons l'étape de normalisation, qui transforme le langage de programmation en langage normalisé. Cette transformation est décomposée en trois étapes afin de simplifier les preuves de correction. Pour établir la préservation de la sémantique, il est nécessaire de démontrer que les trois passes préservent certaines propriétés statiques et dynamiques du langage. En particulier, il faut prouver le lien entre le typage des horloges et la sémantique dynamique pour pouvoir raisonner sur la suite de la compilation.
Origine : Fichiers produits par l'(les) auteur(s)
