Formal Methods of Software Design
This course is freely available for any university to offer, and for any individual to take on their own.
"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.
Motivations for this course are here,
here,
here,
here
and here p.10,
and this video at 4:24.
Read comments on this course's formal methods.
Get the course textbook. (It is also available from Springer Publishing, but that edition is expensive and way out of date.)
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 a link to the lecture visuals, then the lecture time [minutes:seconds].
Finally, there is a suggested exercise or two from the textbook.
Lecture segment 0 and transcript 0 and visuals 0 [11:59] Introduction; try Exercises 0 and 2
Lecture segment 1 and transcript 1 and visuals 1 [30:29] Binary Theory; try Exercises 14 and 17
Lecture segment 2 and transcript 2 and visuals 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 and visuals 3 [14:23] Collections: Bunches and Sets; try Exercises 49 and 53
Lecture segment 4 and transcript 4 and visuals 4 [27:24] Sequences: Strings and Lists; try Exercise 64
Lecture segment 5 and transcript 5 and visuals 5 [10:30] Functions; try Exercise 69
Lecture segment 6 and transcript 6 and visuals 6 [11:12] Quantifiers; try Exercise 80
Lecture segment 7 and transcript 7 and visuals 7 [19:00] Function Fine Points; try Exercise 105
Lecture segment 8 and transcript 8 and visuals 8 [30:31] Specification; try Exercise 125
Lecture segment 9 and transcript 9 and visuals 9 [28:59] Refinement and Programs; try Exercises 135, 142, and 143
Lecture segment 10 and transcript 10 and visuals 10 [28:54] Time Calculation; try Exercise 159
Lecture segment 11 and transcript 11 and visuals 11 [18:52] Searching; try Exercise 192
Lecture segment 12 and transcript 12 and visuals 12 [21:26] Two Great Examples: Fast Exponentiation and Fibonacci; try Exercise 195
Lecture segment 13 and transcript 13 and visuals 13 [16:10] Space Calculation; try Exercise 290
Lecture segment 14 and transcript 14 and visuals 14 [12:12] Old Theory; try Exercise 300(g)
Lecture segment 15 and transcript 15 and visuals 15 [16:42] Scope and Data Structures; try Exercise 315
Lecture segment 16 and transcript 16 and visuals 16 [27:38] Control Structures; try Exercise 248(a)
Lecture segment 17 and transcript 17 and visuals 17 [23:06] Mid-Course Review; try Exercise 243
Lecture segment 18 and transcript 18 and visuals 18 [14:11] Time and Space Dependence and Assertions; try Exercise 332
Lecture segment 19 and transcript 19 and visuals 19 [16:14] Subprograms and Aliasing; try Exercise 337
Lecture segment 20 and transcript 20 and visuals 20 [23:35] Probabilistic Programming; try Exercises 341 and 346
Lecture segment 21 and transcript 21 and visuals 21 [14:33] Functional Programming; try Exercise 177
Lecture segment 22 and transcript 22 and visuals 22 [19:04] Recursive Data Definition; try Exercise 390
Lecture segment 23 and transcript 23 and visuals 23 [8:22] Recursive Program Definition; try Exercise 407(a,b,c)
Lecture segment 24 and transcript 24 and visuals 24 [27:24] Data Theory Design; try Exercise 424
Lecture segment 25 and transcript 25 and visuals 25 [12:13] Program Theory Design; try Exercise 440
Lecture segment 26 and transcript 26 and visuals 26 [21:38] Data Transformation; try Exercise 467
Lecture segment 27 and transcript 27 and visuals 27 [11:46] Limited Queue; try Exercise 470
Lecture segment 28 and transcript 28 and visuals 28 [13:03] Concurrent Composition; try Exercise 479
Lecture segment 29 and transcript 29 and visuals 29 [21:17] Sequential to Concurrent Transformation; try Exercise 489
Lecture segment 30 and transcript 30 and visuals 30 [16:00] Interactive Variables; try Exercise 498
Lecture segment 31 and transcript 31 and visuals 31 [19:20] Communication Channels; try Exercise 518
Lecture segment 32 and transcript 32 and visuals 32 [14:54] Local Channel Declaration, Deadlock, Broadcast; try Exercise 525
Lecture segment 33 and transcript 33 and visuals 33 [19:00] Final Review; try Exercise 262
total lecture time [10:34:23]