Sémantique et preuve des programmes
Description
La valeur d’un modèle tient au sens qu’il porte et aux outils qu’on
peut lui appliquer. Il est primordial que les différents outils
interprètent un modèle donné de la même façon. Ce cours présente les
techniques sémantiques qui permettent de définir le sens d’un langage,
et donc le sens des modèles exprimés dans ce langage. On y verra comment
modéliser la syntaxe abstraite d’un langage (en connexion avec le cours
de traitement des langages), choisir un domaine sémantique (en général
une logique), et comment établir une correspondance entre les éléments
syntaxiques et les éléments sémantiques. Les différents styles de
sémantiques (opérationnel, dénotationnel, axiomatique) seront présentés,
ainsi que les relations de consistance et de complétude relatives.
Ce cours s’appuie sur le cours de logique et systèmes déductifs, et suit
une approche pragmatique avec une mise en œuvre concrète des concepts et
des méthodes dans l’assistant de preuve Isabelle/HOL. 16 heures de
travail personnel sont dédiées à la prise en main de l’outil (tutoriel à
suivre) et à des exercices. Deux créneaux de 3 heures en présentiel
sont consacrés à une pratique encadrée (travaux pratiques) afin d’ancrer
les notions abstraites dans leur mise en œuvre concrète sur un cas
d’étude. Deux autres créneaux de 3h sont consacrés à la preuve de programmes C avec Frama-C afin de montrer comment les techniques vues dans ce cours s'appliquent dans un contexte industriel.
Période(s) du cours
Prérequis
Syllabus
7 créneaux de 3h (21 HPE).
- Créneau 1 : Introduction, initiation à Isabelle/HOL
- Logique d'ordre supérieur
- Principes fondamentaux d'Isabelle/HOL
- Tutoriel sur la définition de types inductifs, de fonctions et les techniques de preuve.
- Créneau 2 : Sémantique opérationnelle (avec exercices sur machine)
- Syntaxe et sémantique
- Rappel sur le langage Niklaus
- Modélisation de la syntaxe abstraite de Niklaus en Isabelle/HOL
- Choix du domaine sémantique
- Correspondance syntaxe abstraite <-> domaine sémantique
- Sémantique des expressions Niklaus
- Approche fonctionnelle, problème de la terminaison
- Approche inductive
- Sémantique à petits pas ou à grands pas
- Sémantique à grands pas de Niklaus
- Créneau 3 : Sémantique dénotationnelle
- Problème des définitions récursives
- Définitions récursives de la factorielle
- Fonctionnelles et points fixes
- Application à la sémantique dénotationnelle du while
- Sémantique dénotationnelle de Niklaus
- Créneau 4 : sémantique axiomatique
- Triplets de Hoare
- Validité et dérivabilité
- Plus faible précondition, notion d'invariant
- Sémantique axiomatique de Niklaus
- Preuves de programmes
- Créneau 5 : Finalisation des projets
- Compléments sur les définitions sémantiques
- Tactiques de preuve
- Déblocage sur des problèmes techniques
- Finalisation des exercices sur la simplification d'expressions arithmétique et sur les expressions régulières
- Créneaux 6 et 7 : bureau d'étude Frama-C (Nikolaï Kosmatov)
- Preuve de programmes C
- Preuve de programmes C
Composition du cours
- Site web présentant le matériel du cours ainsi que des éléments d'initiation et d'approfondissement
- Auto-formation aux outils par un tutoriel afin d'être prêt à suivre les cours
- Cours magistraux pour présenter les concepts
- Cours sur machine pour mettre en œuvre les concepts avec l'assistance d'un enseignant
- Bureaux d'étude avec réalisations concrètes pour mettre en œuvre les concepts et se les approprier