CSC465/2104 2007 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 best motivation for this course is written here
and here. Please read them.
bulletin board
course information
The textbook 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.
study questions
assignment cover page
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.
announcements of general interest to undergraduates (not course related)
a warning about cheating