Dr.-Ing. Robert L. Baber
Office: ITC (T16)-168, tel. ext. 27874
Email: Baber@McMaster.CA
Office hours: Thursdays 14.30-16.30 or by appointment or when available

2. Course Structure

Three 50-minute lectures weekly:
Mondays and Thursdays 9.30-10.20, Tuesdays 10.30-11.20, room ABB/271

3. Teaching Assistant

One teaching assistant has been allocated to this course and will be available for consultation.

4. Prerequisite and Corequisite Knowledge

The formal prerequisite for this topic is registration in Level IV Software Engineering, Level IV Computer Science or graduate studies. General mathematical knowledge (especially basic concepts and definitions of sets, functions, images and preimages of a set under a function, and Boolean algebra) and familiarity with one or more procedural programming languages is presumed. All students should review the general mathematical background material (see http://www.cas.mcmaster.ca/~baber/Courses/46L03/MathFund.pdf) at the beginning of the term.

Students are also expected to be able to reformulate word problems into mathematical terminology with facility. The document Translating English to Mathematics (at http://www.cas.mcmaster.ca/~baber/Courses/General/EnglToMath.pdf) may help them to improve their abilities in this area.

5. Calendar Description

Mathematical model of a program and its execution, preconditions, postconditions, partial, semi-total and total correctness, proof rules and their application both to verifying and to designing programs. While a complete theoretical foundation is presented, the motivation, orientation and ultimate goal of this course are the practical application of the material covered.

6. Mission

Characteristic of every engineering field is a theoretical, scientific foundation upon which most of the engineer’s work is based. Engineers apply this foundation continually, systematically and almost subconsciously in the course of performing their professional work. This basis for engineering work is a prerequisite for achieving the reliability of designs to which engineers, their clients and society have become accustomed.

The mission of this course is to present such a theoretical, scientific foundation for designing software and for proving mathematically that it is correct, i.e. that it satisfies its specification. In particular, this course presents a mathematical model of a program and its execution and shows how it can be practically applied to design a program to satisfy a given specification and to prove that the program does, in fact, satisfy the specification.

Emphasis will be placed on designing and verifying individual subprograms and routines.

7. Objectives

The students will learn how a mathematically based approach enables one to design correct software effectively in practice. In particular, after completing this course the students will be able

• to prove mathematically that a given program satisfies its specification,
• to derive a precondition for a given program and postcondition and
• to design a program to satisfy a given specification, deriving substantial parts of the program mathematically.

For undergraduate students, the grade for the course will be made up of the grades for assignments, two class tests and the final examination weighted as follows:

• assignments, 10%
• two class tests, 15% each
• final examination, 60%

• assignments, 10%
• design and analysis project, 10%
• two class tests, 10% each
• final examination, 60%

Each assignment will be graded on a coarse scale (an integer from 0 to 4). The assignments will be reviewed (and in some cases graded) in class. Assignments will be individual exercises and possibly a small number of group exercises.

All students must be prepared to present their solutions to the assignments in class. A student's grade on an assignment can be affected positively or negatively by the student's presention of the solutions.

9. Literature

Notes and exercises prepared by the instructor will be distributed to the students via the course's web site at http://www.cas.mcmaster.ca/~baber/Courses/46L03.

In addition, the following literature is recommended as ancillary reading:

• Abrial, J.-R., The B-Book: Assigning Programs to Meanings, Cambridge University Press, Cambridge, 1996.
• * Baber, Robert L., Software Reflected: The Socially Responsible Programming of Our Computers, North-Holland, Amsterdam, 1982.
• * Baber, Robert L., The Spine of Software: Designing Provably Correct Software — Theory and Practice, John Wiley & Sons, Chichester, 1987.
• * Baber, Robert L., Error-free Software: Know-How and Know-Why of Program Correctness, John Wiley & Sons, Chichester, 1991.
• * Baber, Robert L., Praktische Anwendbarkeit mathematisch rigoroser Methoden zum Sicherstellen der Programmkorrektheit, (in German), Walter de Gruyter, Berlin, 1995.
• Backhouse, Roland C., Program Construction and Verification, Prentice-Hall International, Englewoods Cliffs, N. J. 1986.
• Dijkstra, Edsger W., A Discipline of Programming, Prentice-Hall, Inc., Englewood Cliffs, N. J., 1976.
• Gries, David, The Science of Programming, Springer-Verlag, New York, Heidelberg, Berlin, 1981.
• Hoare, C.A.R., "An Axiomatic Basis for Computer Programming", Communications of the ACM, Vol. 12, No. 10, p. 576-580+583, 1969 Oct.
• Hoare, C.A.R. et al., "Laws of Programming", Communications of the ACM, Vol. 30, No. 8, p. 672-686, 1987 Aug. and Corrigenda, Communications of the ACM, Vol. 30, No. 9, p. 770, 1987 Sept.
• Kaldewaij, Anne, Programming: The Derivation of Algorithms, Prentice-Hall International, 1990.
• Loeckx, Jacques; Sieber, Kurt, The Foundations of Program Verification, B. G. Teubner, Stuttgart, und John Wiley & Sons, Chichester, 1984.
• Mills, Harlan D., "The New Math of Computer Programming", Communications of the ACM, Vol. 18, No. 1, p. 43-48, 1975 Jan.

An extensive bibliography of other relevant literature can be found in the book Praktische Anwendbarkeit mathematisch rigoroser Methoden zum Sicherstellen der Programmkorrektheit listed above, p. 201-235.

10. Schedule

The following is a tentative schedule for this term. Changes will be announced in class and/or a revised schedule will be published as required.

September 5 – October 10: Chapters 1 – 5 of the lecture notes and related assignments
Test 1: October 15
October 17 – November 14: Chapters 6 – 8 of the lecture notes and related assignments
Test 2: November 19
November 21 – December 2: Chapters 9 – 10 of the lecture notes and assignments and other material related to the entire course, general review.
Graduate students' project due: November 25
Final examination: during the examination period

11. Announcements

Please refer to http://www.cas.mcmaster.ca/~baber/Courses/46L03/Announcements.html frequently for announcements and news items relevant to this course. Notes and exercises prepared by the instructor will be distributed to the students via the course's web site at http://www.cas.mcmaster.ca/~baber/Courses/46L03.

12. Notes

• Discrimination
"The Faculty of Engineering is concerned with ensuring an environment that is free of all adverse discrimination. If there is a problem that cannot be resolved by discussion among the persons concerned, individuals are reminded that they should contact their Department Chair, the Sexual Harrassment/Anti-Discrimination Officer (SHADO), as soon as possible."
• Academic Dishonesty
"Students are reminded that they should read and comply with the Statement on Academic Ethics and the Senate Resolutions on Academic Dishonesty as found in the Senate Policy Statements distributed at registration and available in the Senate Office."