Formal Methods of Software Design

an online course by Eric Hehner

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, here, and here. Read comments on this course's formal methods.

Get the course textbook. Solutions to exercises are available to course instructors.

There are 34 lectures below for you to watch at your convenience. You may need to zoom in or zoom out in your browser to get the size right. The title panel lasts a few seconds before the lecture starts.

After each lecture segment listed below, there is a link to the visuals used in the lecture. For the purpose of printing the visuals, here they are in a more convenient, compact form, by chapter: 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.

Then there is a link to the lecture transcript, then the lecture time. Finally, there is a suggested exercise or two from the textbook, and there are hundreds more exercises in the textbook for you to choose from. When you have done an exercise, send your solution to the course instructor, and you will receive a solution to compare with your solution. If you choose to typeset your assignments in LaTeX, here is a helpful set of macros, courtesy of Albert Lai.

The mid-term test and final exam must be arranged with the course instructor. To help you, here are some study questions. And here is some tutorial material for Chapter 1, Chapter 3, and Chapter 4.

Lecture segment 0, visual 0, and transcript 0 [11:28] Introduction; try Exercise 0
Lecture segment 1, visual 1, and transcript 1 [26:17] Boolean Theory; try Exercises 5 and 12
Lecture segment 2, visual 2, and transcript 2 [11:09] Boolean Theory continued, Number Theory, Character Theory; try Exercises 2(f,m,p,s,u) and 16
Lecture segment 3, visual 3, and transcript 3 [14:04] Collections: Bunches and Sets; try Exercises 41 and 44
Lecture segment 4, visual 4, and transcript 4 [25:13] Sequences: Strings and Lists; try Exercise 53
Lecture segment 5, visual 5, and transcript 5 [10:06] Functions; try Exercise 55
Lecture segment 6, visual 6, and transcript 6 [11:22] Quantifiers; try Exercise 63
Lecture segment 7, visual 7, and transcript 7 [17:22] Function Fine Points; try Exercise 81
Lecture segment 8, visual 8, and transcript 8 [27:45] Specification; try Exercise 99
Lecture segment 9, visual 9, and transcript 9 [11:03] Refinement; try Exercises 116 and 120
Lecture segment 10, visual 10, and transcript 10 [23:41] Program Development; try Exercise 125
Lecture segment 11, visual 11, and transcript 11 [26:14] Time Calculation; try Exercise 133
Lecture segment 12, visual 12, and transcript 12 [17:38] Searching; try Exercise 158
Lecture segment 13, visual 13, and transcript 13 [21:27] Two Great Examples: Fast Exponentiation and Fibonacci; try Exercise 161
Lecture segment 14, visual 14, and transcript 14 [14:47] Space Calculation; try Exercise 215
Lecture segment 15, visual 15, and transcript 15 [15:18] Scope and Data Structures; try Exercise 263
Lecture segment 16, visual 16, and transcript 16 [29:28] Control Structures; try Exercise 208(a)
Lecture segment 17, visual 17, and transcript 17 [23:20] Mid-Course Review; try Exercise 202
Lecture segment 18, visual 18, and transcript 18 [13:44] Time and Space Dependence and Assertions; try Exercise 276
Lecture segment 19, visual 19, and transcript 19 [15:04] Subprograms and Aliasing; try Exercise 274
Lecture segment 20, visual 20, and transcript 20 [24:39] Probabilistic Programming; try Exercises 279 and 280
Lecture segment 21, visual 21, and transcript 21 [15:00] Functional Programming; try Exercise 144
Lecture segment 22, visual 22, and transcript 22 [18:21] Recursive Data Definition; try Exercise 309
Lecture segment 23, visual 23, and transcript 23 [8:32] Recursive Program Definition; try Exercise 321(a,b,c)
Lecture segment 24, visual 24, and transcript 24 [27:26] Data Theory Design; try Exercise 338
Lecture segment 25, visual 25, and transcript 25 [12:05] Program Theory Design; try Exercise 351
Lecture segment 26, visual 26, and transcript 26 [21:40] Data Transformation; try Exercise 365
Lecture segment 27, visual 27, and transcript 27 [11:57] Limited Queue; try Exercise 372
Lecture segment 28, visual 28, and transcript 28 [13:47] Independent Composition; try Exercise 375
Lecture segment 29, visual 29, and transcript 29 [21:04] Sequential to Parallel Transformation; try Exercise 381
Lecture segment 30, visual 30, and transcript 30 [15:49] Interactive Variables; try Exercise 386
Lecture segment 31, visual 31, and transcript 31 [19:41] Communication Channels; try Exercise 410
Lecture segment 32, visual 32, and transcript 32 [15:35] Local Channel Declaration, Deadlock, Broadcast; try Exercise 414
Lecture segment 33, visual 33, and transcript 33 [18:45] Final Review; try Exercise 226
total lecture time [10:01:10]