CSC465/2104 2009 Fall
Formal Methods of Software Design
The use of logic as an aid to programming. Formal semantics of programming
languages: imperative programs, functional programs, parallel processes,
communicating processes. Theorems about programs: transformations,
reformations, state theorems. Refinement
by steps and by parts. Recursion and the least fixed-point
construction. Axioms of data types; data
refinement.
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 will also look at parallel and interacting processes, and also
at probabilistic programming. Along the way, we define the formal
semantics of 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.
The three best motivations for this course are written here,
here,
and here. Some comments on this course's formal methods are
here. Please read them.
bulletin board
course information
study questions
assignment cover page
The textbook and lecture visuals can be downloaded free here.
If you choose to typeset your assignments in LaTeX, here is a helpful set of macros, courtesy of Albert Lai.
Marks so far are here. To see them, you need a special username and password, which are announced in class.
If you have a complaint about the marking, write your complaint on a piece of paper,
and hand it and the assignment to a TA or to the prof for remarking.
a warning about cheating