Ce cours s’adresse à des ingénieurs en informatique ayant une expérience du développement logiciel dans un langage de programmation usuel. Le cours comporte sept volets pour enseigner :
- la base de la théorie des types,
- comment décrire des algorithmes,
- comment exprimer les propriétés attendues,
- comment prouver que les propriétés sont satisfaites,
- comment tirer parti de la modularité logique,
- comment obtenir du logiciel exécutable,
- un panorama des applications complètes et réalistes.
Il s’inspire du cas de figure des bases de données pour montrer comment appliquer Coq pour modéliser des opérations sur des ensembles de données (intersection, union, sélection). Les propriétés logiques illustrent comment plusieurs séquences d’opérations peuvent aboutir au même résultat. Les techniques de preuves se concentrent sur les connecteurs logiques de base et sur la technique qui permet de raisonner sur des ensembles de taille non bornée: la preuve par récurrence. Le cours montre également comment des choix de structure de données différents permettent d’obtenir des programmes plus ou moins efficaces, tout en préservant la correction des opérations effectuées. Les techniques pour obtenir du code exécutable à partir des modèles formels sont également présentées. Enfin, le cours effectue un panorama des applications majeures qui ont été développées avec Coq et qui servent de base à des projets de plus en plus ambitieux.
À la fin du cours, les participants auront compris comment les techniques de modélisation, de description des propriétés, de preuve, et de production de logiciel dérivé peuvent être appliquées sur des projets logiciels.
