"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 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 four best motivations for this course are written here, here, here, and here. Read comments on this course's formal methods.

Get the course textbook. Here are pages 234,..247 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 formal proof (Chapter 1), quantifiers (Chapter 3), one-point laws (Chapter 3), specifications (Chapter 4), and proof strategy (Chapter 4). Here are the solutions to the exercises.

This course comes in two versions: for-credit, and not-for-credit.

For-Credit: You must be registered at a university that offers this course. There is a start date and a finish date for the course. There are tests during the term and an exam at the end. The times and places of the tests and exam are set by the university.

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 exams. I would be happy to hear from you, if you don't mind emailing me.

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 classroom time and an online chat room for students to discuss the exercises and course material with the course instructor and with each other. In the not-for-credit version, you may email questions to me. If you use a word processor to compose your solutions, here are the symbols you need. If you choose to typeset your solutions in LaTeX, here is a helpful set of macros. When you have done an exercise, compare your answer to the solution online. (If you just look up the solution without trying the exercise first, you will not get the full benefit of the exercise.) Solutions to exercises will not be graded.

There are 34 lectures below for you to watch at your convenience. (There are also lectures for this course on YouTube, but those lectures are out of date.) After each lecture segment listed below, there is a link to the lecture transcript, then the lecture time [minutes:seconds]. Finally, there is a suggested exercise or two from the textbook.

Lecture segment 0 and transcript 0 [12:00] Introduction; try Exercises 0 and 2

Lecture segment 1 and transcript 1 [30:29] Binary Theory; try Exercises 14 and 17

Lecture segment 2 and transcript 2 [12:22] 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:09] Collections: Bunches and Sets; try Exercises 49 and 53

Lecture segment 4 and transcript 4 [27:24] Sequences: Strings and Lists; try Exercise 64

Lecture segment 5 and transcript 5 [10:49] Functions; try Exercise 69

Lecture segment 6 and transcript 6 [11:49] Quantifiers; try Exercise 80

Lecture segment 7 and transcript 7 [18:43] Function Fine Points; try Exercise 105

Lecture segment 8 and transcript 8 [30:32] Specification; try Exercise 125

Lecture segment 9 and transcript 9 [28:59] Refinement and Programs; try Exercises 135, 142, and 143

Lecture segment 10 and transcript 10 [28:54] Time Calculation; try Exercise 159

Lecture segment 11 and transcript 11 [18:52] Searching; try Exercise 192

Lecture segment 12 and transcript 12 [21:49] Two Great Examples: Fast Exponentiation and Fibonacci; try Exercise 195

Lecture segment 13 and transcript 13 [16:44] Space Calculation; try Exercise 290

Lecture segment 14 and transcript 14 [12:13] Old Theory; try Exercise 300(g)

Lecture segment 15 and transcript 15 [16:42] Scope and Data Structures; try Exercise 315

Lecture segment 16 and transcript 16 [27:38] Control Structures; try Exercise 248(a)

Lecture segment 17 and transcript 17 [23:06] Mid-Course Review; try Exercise 243

Lecture segment 18 and transcript 18 [14:12] Time and Space Dependence and Assertions; try Exercise 332

Lecture segment 19 and transcript 19 [16:35] Subprograms and Aliasing; try Exercise 337

Lecture segment 20 and transcript 20 [25:36] Probabilistic Programming; try Exercises 341 and 346

Lecture segment 21 and transcript 21 [15:15] Functional Programming; try Exercise 177

Lecture segment 22 and transcript 22 [19:06] Recursive Data Definition; try Exercise 390

Lecture segment 23 and transcript 23 [8:23] Recursive Program Definition; try Exercise 407(a,b,c)

Lecture segment 24 and transcript 24 [27:45] Data Theory Design; try Exercise 424

Lecture segment 25 and transcript 25 [12:35] Program Theory Design; try Exercise 440

Lecture segment 26 and transcript 26 [21:39] Data Transformation; try Exercise 467

Lecture segment 27 and transcript 27 [11:46] Limited Queue; try Exercise 470

Lecture segment 28 and transcript 28 [12:59] Concurrent Composition; try Exercise 479

Lecture segment 29 and transcript 29 [21:11] Sequential to Concurrent Transformation; try Exercise 489

Lecture segment 30 and transcript 30 [16:00] Interactive Variables; try Exercise 498

Lecture segment 31 and transcript 31 [19:47] Communication Channels; try Exercise 518

Lecture segment 32 and transcript 32 [15:20] Local Channel Declaration, Deadlock, Broadcast; try Exercise 525

Lecture segment 33 and transcript 33 [19:05] Final Review; try Exercise 262

total lecture time [10:40:29]