Il est important d'installer Isabelle et de faire ce tutoriel avant la première séance.
Séance 1/4 le 18 mars 2024
Pensez à faire le tutoriel et les exercices (et à les rendre sur le dépôt git) !
- Introduction
- Syntaxe abstraite de Niklaus : expressions, instructions
- Sémantique naïve par interprétation
- Sémantique opérationnelle de Niklaus
- Exemples (curryfication et définition de fonctions inductives)
Séance 2/4 le 25 mars 2024
- Correction des exercices du tutoriel
- Sémantique dénotationnelle
- Sémantique des définitions récursives
- Points fixes, théorème de Knaster-Tarski
Exercice à rendre sur le dépôt git (avant la dernière séance) : Simplification d'expression
Séance 3/4 du 26 mars 2024
- Sémantique axiomatique, triplets de Hoare.
- Plus faible précondition, Consistance et complétude
- Exemple de preuve de programme Niklaus
- Exercice sur la compilation d'expressions à faire en cours et à rendre sur le dépôt git.
- Exercice de modélisation (optionnel) : expressions régulières à rendre sur le dépôt git
Pour un exemple assez simple de preuve de correction d'un compilateur,
vous pouvez consulter l'épisode Program correctness
de la chaîne Youtube Computerphile.
J'ai fait la preuve de la correction du mini compilateur sur cette page.
Séance 4/4 du 9 avril 2024
- Compléments
- Aide pour finir les exercices à rendre
Récapitulatif des exercices à rendre avant le 19 avril 2024
- Fichiers complétés en cours (sémantiques, récursion etc.)
- Exercices :
- Tutoriel et exercices associés
- Simplification d'expressions Niklaus
- Compilation d'expressions Niklaus
- Facultatif : Modélisation d'expressions régulières
Séances Frama-C les 5 et 15 avril 2024
Attention, projet à rendre aussi sur ce sujet.