Page de ressources pour le DIU-EIL 2019

Bloc 2 : Algorithmique (partie : correction d'algorithmes)

Descriptif du cours 1 (16 mai 2019)

• correction totale = correction partielle + terminaison
• spécification du calcul d'extraction de la racine carrée : un exemple où spécifier est moins compliqué et moins source d'erreur que de programmer la solution
• exemple de programme dont il n'est pas évident d'établir la sémantique
  int x,y;
x:=x+y;
y:=x-y;
x:=y-x;

• division euclidienne par soustractions successives (programme, précondition/postcondition, variant et invariant)
• multiplication par addition (programme, variant et invariant)
  
• 4 programmes dont on pourrait penser qu'ils calculent tous la factorielle de leur argument n
• le drapeau hollandais (description puis discussion autour d'un variant et d'un invariant possibles)

Descriptif du cours 2 (1er juillet 2019)

• Logique de Hoare
• Quelques exemples de programmes et leurs preuves de correction en Why3 (sommes des n premiers entiers, multiplication russe, racine carrée entière, recherche dichotomique, tri par insertion)

Ressources utiles

• cours d'ingénierie de la preuve en Master Informatique (notamment les slides n°7 à n°25)
• Cours de Benjamin Wack sur les preuves d'algorithmes et sur la logique de Hoare
• livre Introduction to Algorithms, Third Edition, Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest and Clifford Stein.
  Le livre en français s'appelle "introduction à l'algorithmique" et est disponible dans toutes les bonnes bibliothèques.
• Exposé de Jean-Christophe Filliâtre sur la Vérification déductive de programmes
• livre Numérique et Sciences Informatiques - 30 leçons et 300 exercices corrigés - Première - Nouveaux programmes (à paraître le 6 août 2019)

• l'assistant de preuve Coq
• l'environnement pour l'analyse modulaire de programmes C Frama-C
• l'environnement de preuves de programmes Why3 et ses exemples en Python