Programmation de confiance

Programmation de confiance

En pratique

Nature
Unité d'enseignement
ECTS
5
Type d'enseignement
Présentiel
Volume horaire de TP
20
Volume horaire de TD
16
Volume horaire de CM
14
Langue d'enseignement
Français

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
    1. 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.
Dernière modification : lun, 25/05/2020 - 19:52