Learning outcomes

By the end of the course the students will be able to reason formally about the correctness of a small program et will be able to compute its complexity. They will master the principles of Hoare logic as a proof technique; and they will have an understanding of some basic algorithmic techniques.

Goals

The objective of this course is to introduce students to formal reasoning about programs (in terms of correction and complexity) and to teach a rigorous method of program construction for programming in the small.

 

Content

This course introduces the students to formal reasoning about programs. We study the principal concepts behind program specifications. We learn techniques that allow to prove that a program is correct with respect to a specification. Building on these techniques we derive a methodology for constructing (small) programs that are automatically correct. We also introduce the basic notions behind computing the complexity (time and memory) of a program et we study some search and sort algorithms.

Assessment method

The evaluation of the students is done on the basis of two aspects. 
1) Participation in the exercise sessions.  In particular, the level of understanding of the concepts seen in the theoretical lectures is evaluated using the exercises done in preparation and the exercises done in the session.
2) The realization of the individual assignment throughout the semester.  All of the remittances made within the framework of this work are evaluated. In particular, the technical quality of the achievements, the level of understanding of the concepts and techniques studied in the course, and the quality of the reporting in relation to the instructions given in the assignment are evaluated.
 

Sources, references and any support material

  • 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.

Language of instruction

Français
Training Study programme Block Credits Mandatory
Bachelier en sciences informatiques (horaire décalé) Standard 0 10
Bachelier en sciences informatiques (horaire décalé) Standard 2 10