Formal Methods of Software Design
"Formal methods of software design" means using mathematics to write
error-free programs. The mathematics needed is not complicated; it's
just basic logic. The word "formal" means the use of a formal
language, so that the program logic can be machine checked. Our
compilers already tell us if we make a syntax error, or a type error, and
they tell us what and where the error is. Formal methods take the next
step, telling us if we make a logic error, and they tell us what and where
the error is. And they tell us this as we make the error, not after the
program is finished. It is good to get any program correct while writing
it, rather than waiting for bug reports from users. It is absolutely
essential for programs that lives will depend on.
The course begins by introducing (or reviewing) the basic logic that will
be used in the course as an aid to programming. Then we look at formal
specifications, and how they are refined to become programs. At each
refinement step, there is a small theorem to be proven (that the step is
correct), so that at the end, the program is correct. Most of the course
uses just those programming constructs that are common to most
programming languages (assignment statement, if statement, array). We
also look at parallel and interacting processes, at probabilistic
programming, and functional programming. Along the way, we
formally define the language features we use (both execution control and
data structures). The emphasis is on program development to meet
specifications, and on program modifications that preserve correctness,
rather than on verification after a program is finished.
Prerequisites: some programming experience, and some mathematical ability.
The three best motivations for this course are written here,
and here. Read comments on this course's formal methods.
Get the course textbook.
Here are pages 231,..244 in case you would like to print the laws, precedence table, and distributing operators.
Here are some study questions.
And here is some tutorial material for Chapter 1,
and Chapter 4.
Solutions to exercises are available to course instructors.
This course comes in two versions: for-credit, and not-for-credit.
For-Credit: You must be registered at a university that accepts this
course. There is a start date and a finish date for the course. There are
three one-hour tests during the term, each worth 20%, and a two-hour exam at the end, worth 40%.
The times and places of the tests and exam are set by the university.
The tests and exam will include the laws from the back of the textbook: pages 231,..244.
In addition, you may bring into the tests and exam one letter-sized (or A4) piece of paper with
anything you like written (or typed) on both sides. No other aids are
allowed. For each question, a blank answer is worth approximately
33%; from that, marks will be awarded for relevant and correct
information, and marks will be deducted for irrelevant or incorrect
information. The graded tests will be given back; the graded exam will
not be given back.
Not-For-Credit: You may start the course whenever you like, proceed at
your own pace, and finish whenever you like. There are no tests or
Whether you are taking the course for-credit or not-for-credit, it is very
valuable for your understanding of the course material to do written
exercises (assignments) as you go through the course. With each lecture
segment, there is a suggested small exercise or two from the textbook,
and there are hundreds more exercises in the textbook for you to choose
from. You may work on them by yourself or in a group. In the
for-credit version, there is an online chat room for students to discuss the
exercises and course material with each other. In the not-for-credit
version, you may email questions to the course instructor. If you choose
to typeset your solutions in LaTeX, here is a helpful set of macros.
When you have done an exercise, send your solution to the course
instructor by email, and you will receive a solution by email to compare
with your solution. Solutions to exercises will not be graded.
There are 34 lectures below for you to watch at your convenience.
After each lecture segment listed below, there is a link to the lecture transcript, then the lecture time.
Finally, there is a suggested exercise or two from the textbook.
If you want to print the lecture visuals, here they are:
visuals for Chapter 0,
visuals for Chapter 1,
visuals for Chapter 2,
visuals for Chapter 3,
visuals for Chapter 4,
visuals for Chapter 5,
visuals for Chapter 6,
visuals for Chapter 7,
visuals for Chapter 8,
visuals for Chapter 9.
Lecture segment 0 and transcript 0 [11:56] Introduction; try Exercises 0 and 2
Lecture segment 1 and transcript 1 [29:29] Binary Theory; try Exercises 14 and 17
Lecture segment 2 and transcript 2 [11:16] Binary Theory continued, Number Theory, Character Theory; try Exercises 6(f,m,p,s), 7(c), and 22
Lecture segment 3 and transcript 3 [14:49] Collections: Bunches and Sets; try Exercises 49 and 53
Lecture segment 4 and transcript 4 [27:06] Sequences: Strings and Lists; try Exercise 62
Lecture segment 5 and transcript 5 [10:31] Functions; try Exercise 64
Lecture segment 6 and transcript 6 [12:34] Quantifiers; try Exercise 73
Lecture segment 7 and transcript 7 [19:02] Function Fine Points; try Exercise 97
Lecture segment 8 and transcript 8 [30:26] Specification; try Exercise 116
Lecture segment 9 and transcript 9 [10:59] Refinement; try Exercises 137 and 143
Lecture segment 10 and transcript 10 [26:11] Program Development; try Exercise 142
Lecture segment 11 and transcript 11 [30:43] Time Calculation; try Exercise 156
Lecture segment 12 and transcript 12 [20:28] Searching; try Exercise 186
Lecture segment 13 and transcript 13 [22:27] Two Great Examples: Fast Exponentiation and Fibonacci; try Exercise 189
Lecture segment 14 and transcript 14 [15:15] Space Calculation; try Exercise 252
Lecture segment 15 and transcript 15 [17:52] Scope and Data Structures; try Exercise 297
Lecture segment 16 and transcript 16 [31:09] Control Structures; try Exercise 242(a)
Lecture segment 17 and transcript 17 [25:05] Mid-Course Review; try Exercise 237
Lecture segment 18 and transcript 18 [13:49] Time and Space Dependence and Assertions; try Exercise 311
Lecture segment 19 and transcript 19 [15:10] Subprograms and Aliasing; try Exercise 316
Lecture segment 20 and transcript 20 [26:54] Probabilistic Programming; try Exercises 320 and 321
Lecture segment 21 and transcript 21 [15:16] Functional Programming; try Exercise 172
Lecture segment 22 and transcript 22 [18:17] Recursive Data Definition; try Exercise 356
Lecture segment 23 and transcript 23 [8:50] Recursive Program Definition; try Exercise 370(a,b,c)
Lecture segment 24 and transcript 24 [29:29] Data Theory Design; try Exercise 387
Lecture segment 25 and transcript 25 [12:35] Program Theory Design; try Exercise 400
Lecture segment 26 and transcript 26 [22:33] Data Transformation; try Exercise 417
Lecture segment 27 and transcript 27 [12:03] Limited Queue; try Exercise 423
Lecture segment 28 and transcript 28 [14:23] Independent Composition; try Exercise 435
Lecture segment 29 and transcript 29 [21:00] Sequential to Parallel Transformation; try Exercise 444
Lecture segment 30 and transcript 30 [16:00] Interactive Variables; try Exercise 451
Lecture segment 31 and transcript 31 [20:06] Communication Channels; try Exercise 471
Lecture segment 32 and transcript 32 [15:33] Local Channel Declaration, Deadlock, Broadcast; try Exercise 477
Lecture segment 33 and transcript 33 [19:27] Final Review; try Exercise 256
total lecture time [10:48:35]