Vous êtes ici

  1. Accueil
  2. UE7 - Programmation de confiance

UE7 - Programmation de confiance

UE7 - Programmation de confiance

En pratique :

Volume horaire de cours : 14
Volume horaire global de TD : 16
Volume horaire global de TP : 20
Langue principale : français
Nombre de crédits européens : 5

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
  •  


    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.


    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
     


    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.

     


    Intervenant(s)

    SANDRINE BLAZY-DARMON
    DELPHINE DEMANGE

    Pré-requis

    Pré-requis obligatoires

    Avoir suivi une UE de programmation fonctionnelle et une UE de programmation impérative, ainsi qu’une UE d’initiation à la logique