Acquis d'apprentissage

A l'issue de ce cours l'étudiant sera capable de raisonner formellement sur la correction d'un programme de petite taille et de calculer sa complexité. Et il aura une maîtrise de la logique de Hoare comme technique de preuve de correction. Il maîtrisera les techniques de bases de l'algorithmique.

Objectifs

L'objectif de ce cours est de familiariser l'étudiant à un raisonnement formel sur les programmes (en termes de correction et de complexité) et de lui enseigner une démarche rigoureuse de construction de programmes de petite taille.

Contenu

Ce cours introduit l'étudiant au raisonnement formel par rapport aux programmes. Nous étudions les concepts principaux sous-jacents à la spécification d'un programme. Nous apprenons des techniques qui permettent de prouver la correction d'un programme par rapport à sa spécification. Ensuite, et à partir de ces techniques, nous arrivons à une méthodologie de construction qui permet la réalisation d'un programme à priori correct. Nous introduisons également les notions de base derrière le calcul de complexité (en temps et en espace) d'un programme et on étudie quelques d'algorithmes de recherche et de tri. 

Méthodes d'enseignement

Cours magistraux ex-cathédra accompagnés des séances d'exercices dirigés. Avant  la plupart de ces séances, il est demandé aux étudiants de résoudre un ou plusieurs exercices. Les étudiants amènent le résultat de ce travail en séance où leurs solutions seront évaluées et discutées. Au cours du quadrimestre, un énoncé de travail individuel est également distribué aux étudiants. Sur base de cet énoncé individuel, qui est découpé en plusieurs parties, les étudiants sont invités à remettre un travail individuel découpé de la même façon. Chaque partie du travail fait l'objet d'une nouvelle échéance de remise (la dernière échéance pouvant être fixée à un moment de la session d'examens). A chaque remise, en plus de la partie de travail concernée par l'échéance, les étudiants sont invités à raffiner et remettre la/les partie(s) qu'ils ont produite(s) lors de la/des échéance(s) précédente(s). 

 

 

Méthode d'évaluation

L'évaluation des étudiants se fait sur base de deux aspects. 

  • La participation aux séances de travaux pratiques.  En particulier le niveau de compréhension des concepts vus dans les cours théoriques précédents est évalué à l’aide des exercices faits en guise de préparation  et les exercices faits en séance.
  • La réalisation du travail individuel récapitulatif au long du quadrimestre.  L'ensemble des remises faits dans le cadre de ce travail fait l'objet d'une évaluation. Sont évalués en particulier la qualité technique des réalisations, le niveau de compréhension des concepts et techniques étudiés dans le cours, et la qualité du rapportage en lien avec les consignes données dans l'énoncé.

Sources, références et supports éventuels

  • W. Vanhoof, Méthodes de programmation, notes de cours.
  • K. Rosen, Discrete Mathematics and its applications (Chapter 1, Section 1.1, pp. 1 - 37), 4th edition, McGraw-Hill, 1999.
  • W.A. Wulf, M. Shaw, L.~Flon, and P. Hilfinger, Fundamental Structures of Computer Science. Addison-Wesley, 1981. Chapter 5, pp. 101 -143.
  • D. Gries, The Science of Programming, Springer-Verlag, 1981, Chapters 13 - 16, pp. 163 -215.
  • A. Aho and J. Ullman. Foundations of Computer Science, W.H. Freeman & Company, 1992.
  • K.R. Apt and E.R. Olderog. Verification of Sequential and Concurrent Programs. Springer-Verlag 1997.
  • R.C. BackHouse. Program Construction and Verification. Prentice-Hall, International series in computer science, 1986.
  • E.W. Dijkstra. A discipline of programming. Prentice-Hall, 1976.
  • The Science of Programming
  • Concepts fondamentaux de l'Informatique
  • Méthodes de programmation
  • Verification of Sequential and Concurrent Programs

Langue d'instruction

Formation Programme d’études Bloc Crédits Obligatoire
Bachelier en sciences informatiques (horaire décalé) Standard 0 10
Bachelier en sciences informatiques (horaire décalé) Standard 2 10