En pratique
Description du contenu de l'enseignement
Ce cours introduit les notions de base de la programmation raisonnée (programmation par contrats, typage fort, polymorphisme et ordre supérieur, invariants). Ces notions seront illustrées sur des exemples pratiques de vérification déductive de programmes impératifs.
Cet enseignement est obligatoire. Il s’agit d’un enseignement fondamental (apprentissage de notions communes aux langages de spécification formelle, ainsi que de notions communes à de nombreux langages de programmation) et technologique (mise en pratique de ces notions avec le logiciel de vérification déductive Why3). Il s’appuie sur les cours de programmation impérative et de programmation fonctionnelle de licence, ainsi que sur le cours de génie logiciel de L2, et prépare aux cours de méthodes formelles et de sémantique dispensés en master.
- Programmation par contrats, test de contrats
- Langage de programmation WhyML
- polymorphisme, définitions locales, références, définitions récursives
- Conception et preuve de structures de données ad’hoc
- types algébriques, filtrage, invariants de types
- Invariants de boucle, terminaison de programmes
- Calcul de plus faible précondition
- Vérification déductive avancée au moyen de code fantôme
- Correspondance entre preuve et programme
Organisation
Modalités d'organisation et de suivi
Ce cours comprend de nombreuses séances de travaux pratiques qui permettent de mettre en pratique et d’assimiler les concepts présentés en cours et approfondis en travaux dirigés.
En présentiel
6h par semaine
Travail personnel
2h par semaine
Informations pédagogiques
Compétences à acquérir
À l’issue de ce cours, les étudiants savent spécifier un programme au moyen de contrats. Ils savent également écrire des programmes non triviaux dont ils auront démontré la correction à l’aide d’un outil de l’état de l’art de vérification déductive. Enfin, ils savent exploiter et raisonner sur des structures de données ad’hoc.
Pré-requis recommandés
Avoir suivi une UE de programmation fonctionnelle et une UE de programmation impérative, ainsi qu’une UE d’initiation à la logique
Bibliographie, lectures recommandées
- Sylvain Conchon et Jean-Christophe Filliâtre. Apprendre à programmer avec OCaml. Algorithmes et structures de données. Eyrolles, Septembre 2014.
- John Mac Cormick, Peter Chapin. Building high integrity applications with Spark. Cambridge university press, 2015.
