Logique et preuve

Le module apporte les outils théoriques qui permettent de construire un raisonnement formel et de prouver la terminaison et la correction des algorithmes. Il se déroule en trois parties :

• la théorie de l'induction : définition de types inductifs et preuve par induction, notamment de fonctions récursives ;
• la logique propositionnelle puis la logique du premier ordre, sous l'angle de la théorie des modèles : formaliser un problème et utiliser un solveur pour obtenir une solution ;
• la preuve de programmes : spécification (pré et postconditions), terminaison, invariant de boucle, logique de Hoare.