CSC 236, day section: topics covered so far

Course information sheet in HTML or postscript or PDF. (Includes office hours and similar information.)
E-mail is the best way to reach me and to ask questions.
Photo ID student cards will be required during the midterm and the final exam.

some proof techniques as written in class
You may want to leave the definitions in "chapter 0" of the notes for later, as needed

This is chapter 1 in the notes, but we're starting with the predicate-oriented version of mathematical induction, and doing the set-oriented versions afterwards.

Introduction:

For the purposes of this course, I think of proofs about computer programs as dividing into three categories. The three categories imply different ways of discussing the proofs, and most of all, different notations for expressing the algorithms / programs.
1. Prove things about computer programs in general. Example presented in class: The "halting problem" is uncomputable.
2. Prove things about a particular computer program, using axioms about the semantics of the programming language statements.
3. Prove the correctness of an algorithm. We still probably express this algorithm in a programming language, but we're focusing on the mathematical principles behind the algorithm, and these proofs resemble the other kinds of proofs we're seeing in this course, more than they resemble axiomatic logic proofs.
I'm not exactly sure how to convey the difference I see between types #2 and #3 except by example. Examples to be filled in above when presented (or maybe before).
The use of different notations for proving different kinds of results about computer programs, or indeed for writing computer programs for different kinds of computers or to solve different kinds of problems, is blessed by the "Church-Turing thesis", which I stated as:
All reasonable definitions of "algorithm" are equivalent.

Core material: Chapter 2 of the notes.

Chapters 3 and 4 of the notes
Recurrence relations often come out of the timing analysis of recursive programs, and we want to find a closed form (non-recurrent simple formula) for them where possible.
Structural induction is basically induction on the number of structure-creating rules invoked. Some of the earlier induction material involving induction on the height of trees could have been cast as structural induction on the recursive definition of a tree data structure.
For some structural induction proofs, see some proofs about propositional calculus formulas in chapter 5.

CG is a former ROM building on Queen's Park Crescent. [directions and map]
The midterm covers assignments 1 and 2, and chapters 1 to 4 of the notes, except for structural induction, and except for section 3.2.2 (general solution of a certain form of divide-and-conquer recurrence). (Of course it is a sampling; there will not be questions on every single minor topic.)
STUDENT PHOTO ID CARD REQUIRED.
Aid sheet allowed: One 8½x11" sheet of paper. No calculators, books, personal tutors whispering in your ear, etc.
Seating is assigned. Please check your seat assignment.
If you are trying to find sample old tests on the web or in libraries, you might want to search for "CSC 238" as well as "CSC 236". Also, you will find last fall's midterm for CSC 236 at UTSC on the UTSC web page at the end of http://www.cs.toronto.edu/~vassos/teaching/b36/. Keep in mind that their midterm is two hours, not one; that test would be too long for a midterm in this course here. Also, propositional logic will not be within the scope of our midterm this year.

Vassos Hadzilacos has written a chapter 8 of the notes which is available at http://www.cs.toronto.edu/~vassos/teaching/b36/handouts/ch8.pdf

sample axioms in postscript or PDF (with correction announced in class: avoided confusion by renaming the constant to "prev", because it's the previous value of the variant)
examples presented (with correction announced in class)