Code 3IF2220, 40 HEE, 21 HPE

Contact

Frédéric Boulanger frederic.boulanger@centralesupelec.fr

Site web du cours : https://wdi.centralesupelec.fr/semantique/

Prérequis

Cours de logique et modèles de calcul? de la mention Science du logiciel

Présentation générale

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 modèles de calcul, 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.

Acquis d’apprentissage visés dans le cours

À l'issue de ce cours, les élèves seront capables :

• de donner un sens précis et formel à un modèle,
• de choisir l'approche sémantique adaptée au problème à traiter,
• d'établir les bases de la définition de cette sémantique dans un assistant de preuve,
• d'exploiter cette sémantique pour vérifier des propriétés d'un modèle.

Moyens

Les moyens mis en œuvre pour ce cours combinent tutoriels pour se familiariser avec une problématique, cours magistraux pour définir les concepts, cours sur machine pour les mettre en œuvre avec l'assistance d'un enseignant et bureaux d'étude pour une pratique plus autonome. Un travail personnel d'approfondissement du contenu des bureaux d'étude est attendu.

Description des compétences acquises à l'issue du cours

C1.2 Utiliser et développer les modèles adaptés, choisir la bonne échelle de modélisation et les hypothèses simplificatrices pertinentes pour traiter le problème

• capturer les éléments essentiels à la sémantique des modèles
• les représenter de manière adaptée aux problème posé
• construire plusieurs modèles à différents niveaux d'abstraction et les relier entre eux

C2.1 Avoir approfondi un domaine ou une discipline relatifs aux sciences fondamentales ou aux sciences de l'ingénieur

• maîtriser la logique en tant qu'outil de modélisation

C5.2 Écouter, se faire comprendre et travailler avec des acteurs de culture, d'expérience et compétences variées

• analyser avec rigueur les différents sens que peut avoir un modèle, définir le modèle logique qui correspond à ce que pensent les utilisateurs.

C7.1 Convaincre sur le fond. Être clair sur les objectifs et les résultats attendus. Être rigoureux sur les hypothèses et la démarche. Structurer ses idées et son argumentation. Mettre en évidence la valeur créée

• mettre ses idées au clair grâce à la logique, éviter les modèles monolithiques, structurer les différents niveaux d'abstraction, expliciter les compromis expressivité/résolution.

Contenu

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
  • 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
  • Définition de la 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
  • Définition de la sémantique axiomatique de Niklaus
  • Exemple de preuve de programme
• 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étiques et sur les expressions régulières
• Créneaux 6 et 7 : bureau d'étude Frama-C (Nikolaï Kosmatov)
  • Preuve de programmes C

Méthodes pédagogiques

• Site web présentant le matériel du cours ainsi que des éléments d'initiation et d'approfondissement
• Initiation aux outils par un tutoriel afin d'être prêt pour la suite du cours
• Cours magistraux pour présenter les concepts
• Cours sur machine pour mettre en œuvre les concepts avec l'assistance d'un enseignant
• Réalisations concrètes pour mettre en œuvre les concepts et se les approprier

Méthodes d'évaluation

L'évaluation se fait en contrôle continu sur la qualité des rendus d'exercices (tutoriel, en autres), sur la participation aux cours sur machine et sur les rendus finals.