Descriptif
Dans ce cours, nous apprenons les bases du raisonnement formel sur les programmes avec l’assistant de preuve Rocq. Nous spécifions formellement les langages de programmation, c’est-à-dire leur syntaxe et leur sémantique opérationnelle. Nous formulons également des spécifications de programmes et prouvons que les programmes donnés satisfont à ces spécifications.
Ce cours s'appuie sur la série Software Foundations.
Objectifs pédagogiques
- Utiliser des outils formels pour analyser et vérifier la correction des programmes.
- Acquérir une compréhension solide de la logique de Hoare et de la sémantique opérationnelle.
- Développer des compétences pour la recherche dans les domaines liés à la logique de programmation et à la théorie des langages.
Diplôme(s) concerné(s)
Pour les étudiants du diplôme M1 MPRI - Fondements de l'Informatique
CSC_51051_EP
Pour les étudiants du diplôme Programmes d'échange internationaux
CSC_51051_EP
Pour les étudiants du diplôme Titre d’Ingénieur diplômé de l’École polytechnique
CSC_51051_EP
Format des notes
Numérique sur 20Littérale/grade réduitPour les étudiants du diplôme M1 MPRI - Fondements de l'Informatique
Vos modalités d'acquisition :
TDs : 20%
Projet (avec rapport et soutenance incluant quelques questions de cours) : 80%
Le rattrapage est autorisé (Note de rattrapage conservée)- Crédits ECTS acquis : 5 ECTS
Pour les étudiants du diplôme Programmes d'échange internationaux
Vos modalités d'acquisition :
TDs : 20%
Projet (avec rapport et soutenance incluant quelques questions de cours) : 80%
Pour les étudiants du diplôme Titre d’Ingénieur diplômé de l’École polytechnique
Vos modalités d'acquisition :
TDs : 20%
Projet (avec rapport et soutenance incluant quelques questions de cours) : 80%
Le rattrapage est autorisé (Note de rattrapage conservée)- Crédits ECTS acquis : 5 ECTS
La note obtenue rentre dans le calcul de votre GPA.
Programme détaillé
-
Programmation fonctionnelle en Coq, preuve par induction
-
Preuve par induction, travail avec des données structurées
-
Polymorphisme et fonctions d’ordre supérieur
-
Tactiques dans Coq
-
Logique dans Coq, propositions définies inductivement
-
Applications totales et partielles, programmes impératifs simples
-
Équivalence de programmes
-
Logique de Hoare
-
Sémantique opérationnelle à petits pas
