Course outline, 2002 September 18
Dr.-Ing. Robert L. Baber
Office: ITC (T16)-168, tel. ext. 27874
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.
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.
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
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:
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.
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:
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.
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 assignmentsSee also the reading and study assignments at http://www.cas.mcmaster.ca/~baber/Courses/46L03/Announcements.html.
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
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.