4 séances de 3h mélangeant cours et pratique, 2 séances de 3h sur Frama-C, évaluation sur les éléments produits tout au long du cours.
Objectifs
Ce cours présente les techniques permettant de définir formellement la sémantique d'un langage de modélisation ou de programmation. Il s'appuie sur la pratique avec l'assistant de preuve Isabelle/HOL pour :
- découvrir les différentes approches sémantiques
- apprendre à modéliser en logique HOL
- se constituer une boîte à outils pour la spécification
- découvrir comment les modèles formels mènent à une compréhension fine des systèmes
À titre de fil rouge, ce cours reprend le langage Niklaus du cours de traitement des langages, et lui donne une sémantique opérationnelle et une sémantique dénotationnelle. Une sémantique axiomatique est également disponible, mais elle ne sera pas traitée en cours faute de temps.
Toutes les activités du cours seront enregistrées sur un dépôt git pour chaque élève, qui devra être partagé en mode "Developer" avec moi (Boulanger Frederic, @boulange), afin que je puisse les évaluer.
Programme
- Introduction, rappels du cours de MDE sur la sémantique
- Modélisation de la syntaxe abstraite, définitions sémantiques
- Limites des définitions fonctionnelles
- Définitions par point fixe, sémantique des définitions récursives
- Application à la sémantique opérationnelle à grands pas de Niklaus
- Application à la sémantique dénotationnelle de Niklaus
- Preuves de programmes : spécification, logique de Floyd-Hoare, invariants, plus faible précondition
À faire avant la première séance
Afin de pouvoir profiter des aspects pratiques de ce cours, il est important d'installer Isabelle et de faire ce tutoriel avant la première séance.
Isabelle est installé dans l'image Docker que j'ai préparée et à partir de laquelle vous pouvez lancer facilement un conteneur à l'aide des scripts start-cs3asl.sh (sous MacOS ou Linux) et start-cs3asl.ps1 (pour PowerShell sous Windows), disponibles sur ce dépôt GitHub.
Il faut bien entendu avoir installé Docker avant.
Je vous conseille toutefois d'installer l'application Isabelle dans votre système d'exploitation afin d'avoir de meilleures performances que sous Docker. L'installation est très simple et ne requiert aucune compétence technique particulière.