Teaching directory
Course 2024-2025

Methods in program construction [IHDCB232]

  • 10 credits
  • 30h+30h
  • 1st quarter
Language of instruction: French / Français
Teacher: Vanhoof Wim

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.

Objectives

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.


Prerequisites

Programmation 2 [IHDCB132] et Programmation 1 [IHDCB131]

Co-requisites

Mathématiques pour l'informatique (2e partie) [IHDCB222]

Teaching methods

Lectures accompanied by supervised exercise sessions. Before most of these sessions, students are asked to solve one or more exercises. Students bring the results of their work to the session where their solutions will be evaluated and discussed. During the semester, an individual assignment is also distributed to students. On the basis of this individual assignment, which is divided into several parts, the students are asked to hand in their solution organised in the same way. Each part of the work is subject to a new deadline (the last deadline may be set at some point during the exam session). At each submission, in addition to the part of the work covered by the deadline, students are invited to refine and submit the part(s) they produced during the previous round(s). 
 
 

Evaluations

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.
 

Recommended readings

  • 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

French / Français

Location for course

NAMUR

Organizer

Faculté d'informatique
rue Grandgagnage 21
5000 NAMUR
P. 081725252
F. 081724967
secretariat.info@unamur.be

Degree of Reference

Undergraduate Degree