Teaching the Mathematics of Program Construction
This report surveys the teaching of modules with a content similar to g51mpc (the use of formal mathematical reasoning in the design of reliable computer programs) in the first year at top-rated (excellent in teaching and research) computer science departments in the UK. The report was compiled in December, 2000 from information freely available on the web. Links are provided in each case to the cited information.
A brief summary is as follows: Information freely available on the web shows that the topic of g51mpc is covered in (variously named) modules in the first year in seven of the top computer science departments in the UK (Imperial College, Newcastle, Manchester, Glasgow, Oxford, Cambridge and Warwick). Swansea and Southampton universities do not seem to provide detailed module information. Edinburgh University certainly does not provide detailed module information via the web to outside users. Thus 70% of the top computer science departments certainly do include this material in the first year of their computer science degrees, and the percentage could be 90 to 100%. The conclusion is that there is a clear consensus among the top ranking computer science departments that program correctness should be introduced at the earliest possible opportunity in a computer science degree.
http://www.doc.ic.ac.uk/teaching/under/comp/comput.html#lectures
Logic and Reasoning About Programs are required modules in, respectively, the first and second terms. There are also separate Discrete Mathematics 1 and 2 modules. This is the syllabus for Reasoning about Programs.
“
Reasoning about Programs Lecturer(s): Krysia Broda
To introduce rigorous reasoning in the specification and design of programs.
Induction: mathematical induction, structural induction.
Formal program techniques: specification by pre- and post-conditions, derivation and verification of programs, invariants, proofs of program properties. Conversion of recursion to iteration.
Common algorithms as examples.
”
University of Newcastle Computing Science BSc (Hons) Computing Science - G500
http://www.cs.ncl.ac.uk/degrees/bsc.cs/
This degree includes two first year modules that specifically mention the basic topics studied in g51mpc. The module "Discrete Mathematics for Computing Science" has much in common with g51mpc. It is a compulsory first semester module. The module "Functional and Logic Programming" clearly extends and
reinforces the material covered in the Discrete Mathematics module. (Verbatim) extracts from the module descriptions are shown below.
“
Semester: 1
Aims and Objectives:
(1) understand and be able to use the language of propositional and predicate logic, sets and functions;
(2) be able to establish asssertions using argument forms including structured and mathematical induction;
Semester 2:
Aims:
To provide a basis for learning how to reason about programs within formal models of computation.
”
http://www.cs.man.ac.uk/ugrad/syllabus2000latest/intro/0.html#_Toc481311142
The University of Manchester has three first year modules that specifically mention issues of program correctness in the module descriptions. Once again such issues are introduced immediately in the first semester of year one. The second semester module "Reasoning about programs" corresponds to g51mpc. The module "Software systems design and development" also includes "reasoning about correctness". Below are extracts from the module descriptions.
“
Objectives
- Be able to write informal justifications for the programs they design.
- Ideas of well-foundedness and termination
Duration: 12 weeks in second semester
- Students should be able to (using Tarski's World in the lab) understand sentences in first-order logic, and to write them and translate them to and from English sentences.
- Students should be able to understand first-order logic specification of simple properties of functional and imperative programs.
- Students should be able to reason informally about simple program properties specified in first-order logic.
- Reasoning about simple imperative programs [6]
- Assertions, Hoare triples, examples (3)
- Reasoning about assignment, sequencing, examples (3)
Syllabus
Reasoning about correctness (informal)
”
http://web.comlab.ox.ac.uk/oucl/courses/topics00-01/pp/syllabus.html
The first year of the Computer Science degree is identical to that of the BA in Mathematics and Computer Science. The brief description of the module Procedural Programming (shown below) includes the central notion of an invariant discussed in g51mpc.
“
Imperative programming constructs, with informal treatment of invariants.
Procedures and modules; their use in the design of large programs.
Data structures, including arrays, records and pointers.
Basic tools for program development.
Case studies in design of medium-sized programs.
”
Examination questions set in 1999 and 2000 (http://web.comlab.ox.ac.uk/work/geraint.jones) require students to develop algorithms making explicit use of invariant properties.
http://www.cl.cam.ac.uk/DeptInfo/CST/node24.html
This degree has both a Discrete Mathematics module (extending over two terms) and a Software Engineering II module (second term). The Software Engineering II module is the one that covers material in g51mpc. Its syllabus specifically mentions invariant properties and "showing that a loop is correct by reasoning about its invariant". The relevant information on this module is as follows.
“
The course has two distinct aims. First, it will present a variety of simple methods that an individual can use to write programs systematically. These will include top-down program refinement, systematic design of loops, and a variety of suggestions for improving program reliability. Second, it will survey formal methods for software engineering, introducing the Z specification language and program correctness proofs.
* Program refinement. Top-down design of code. Example: printing a table of squares. Dealing with errors.
* Loop design. The basic while loop. The invariant. Defensive programming. Sentinels. Example of loop design.
* Fault avoidance, or preventing bugs. Slogans: Keep It Simple; Check Everything. The pursuit of efficiency; re-inventing the wheel. Compiler warnings and assert statements.
* Formal methods in software development. Formal specifications and specification languages. Some case studies using formal methods.
* Introduction to the Z specification language. Schemas. The state space: inspecting it, changing it. Spivey's Birthday Book.
* Proving ML programs correct. Structural induction on lists. Associativity of the append function. Generalising the induction formula. Example: equivalence of two functions for list reversal.
At the end of the course, students should
* understand how to use top-down design, recognising its advantages and drawbacks
* be able to describe the main techniques for fault avoidance
* be able to state what formal methods can and cannot do
* be able to write and understand very simple Z schemas
* be able to show that a loop is correct by reasoning about its invariant
* be able to prove simple theorems about functional programs using induction
”
http://www.dcs.gla.ac.uk/courses/teaching/level1/modules/FP1.html
The topic of g51mpc is covered in the second semester, year 1, "Further Programming 1" module. The objectives include:
“
* Be able to annotate programs with assertions, based on an understanding of program text as a document for communication among people.
”
The syllabus includes:
“
Propositional logic; writing loop invariants, pre- and post-conditions.
The professional obligation to produce correct programs.
”
Professor Colin Stirling of Edinburgh University provided me with the web address http://www.dcs.ed.ac.uk/teaching/FirstYearCourses.html but unfortunately this leads to a "You are not authorized to view this page" message.
At Southampton and Swansea Universities I was unable to find detailed information. The following is the information provided at Swansea. http://www.swan.ac.uk/uws/prospectus/ug/courses/compsci.htm
“
The eight Computer Science modules offered in Level 1 cover programming, as well as computer architecture and organisation, software development, logic, discrete mathematics and algorithms. Programming is a fundamental skill in Computer Science, and is introduced through the language Pascal. Later, you will meet other languages, including C, Java, Delphi and Prolog.
”
The information on the 1st year algorithms and computation module mentions developing algorithms strongly suggesting that the material in mpc is covered.
http://www.swan.ac.uk/compsci/undergrad/schemes/Level1.html#aa
“
Algorithms and Computation
There are often many different methods, or algorithms, for solving each problem. This module shows how to develop and analyse algorithms, and systematically choose the correct one for a particular problem. It also explores the limits of computing.
”
At Warwick University logic is introduced in the Discrete Mathematics 1 module in term 1 of the 1st year and program correctness is discussed in the 1st year, 2nd term module Design of Information Structures. Web address and relevant extract are shown below.
http://www.dcs.warwick.ac.uk/pub/course/g500/firstyear.html
“
(i) To gain familiarity with the specification, implementation and use of some standard abstract data types (ADTs) such as linked-lists, stacks, queues, graphs etc.
(ii) To learn some standard algorithms for common tasks (such as searching and sorting) and some elementary methods of measuring the complexity, and of showing the correctness, of algorithms.
(iii) To learn how to program with non-standard ADTs using an object-oriented language.
Learning Outcomes
On completion of the module, a student will:
* be familiar with a range of standard ADTs and how they can be used to accomplish common programming tasks;
* be able to assess the complexity and correctness of simple algorithms, and choose appropriate algorithms for simple tasks; and
* have practical experience of designing user-defined ADTs, and associated algorithms, for a non-standard application.
Content
Types and their properties: simple types in programming languages; relationship between familiar mathematical and program objects of given type. Using predicate logic to state properties of types and their operations in terms of pre- and post-conditions.
Abstract data types: specification of familiar abstract objects (eg complex numbers, sets, sequences, matrices) and their operations, comparison with their implementation using a typical programming language. Specification and implementation of some important standard types (eg strings, stacks and queues).
Algorithms: relationship between data structures and algorithms; some standard algorithms for searching, sorting and pattern matching. Elementary analysis of complexity. Reasoning about the correctness of the implementation of simple algorithms.
”
“
MODULES 6-7: (Core)
·
Mathematics for Computer Scientists
· Discrete Mathematics I
The First Year Mathematics courses provide an essential basis for theory courses and applications in later years. They introduce and motivate important methods of proof and fundamental concepts of set theory, logic, algebra, combinatorics, probability and graph theory; they include some rigorous elementary analysis and a selection of modelling methods drawn from more advanced calculus, logic and linear algebra.
”