This course presents some formal notations that are commonly used for the description of computation and of computing systems, for the specification of software and for mathematically rigorous arguments about program properties.
The following areas of study constitute the backbone of the course. Predicate calculus and natural deduction, inductive definitions of data types as a basis for recursive functions and structural induction, formal language theory (particularly regular expressions, finite state machines and context free grammars), specification languages, propositional programming language semantics, partial correctness and proofs of termination.

Upon completion of this course, the student will be able to do the following:

1. Apply the concepts of standard mathematical logic to produce proofs or refutations of well-formed propositions or arguments phrased in English or in a variety of formal notations (first order logic, discrete mathematics or Hoare Logic).
2. Given a description of a regular language, either in English, as a regular expression or as a grammar, generate a finite state automaton that recognizes that language. Similarly, given a deterministic or nondeterministic automaton, give a description of the language which it accepts.
3. Given an inductive definition of a simple data structure, write a recursive definition of a given simple operation on data of that type. Given some such recursively defined operations, prove simple properties of these functions using the appropriate structural induction principle.
4. Prove simple programs correct using Hoare Logic.
5. Prove correctness and termination of a simple program using the weakest precondition calculus.
6. Specify a simple system using Z.
7. Understand very simple Prolog programs.
8. Design a Turing Machine which will accomplish simple tasks.

Assignments (36%); Tutorials (4%); Quiz (10%); Final Exam (50%)

Thirty one-hour lectures and nine one-hour tutorials.

COMP1110 or COMP1140 or COMP1510  and  MATH1005 or MATH1014 or MATH1116 or enrolment in 4716 or 4717 or 4718

There is no prescribed text for COMP2600, but the following are recommended references. More may be added as the semester progresses.

Grassman, Winfried Karl Grassman & Tremblay, Jean-Paul Logic and Discrete Mathematics: A Computer Science Perspective, Prentice Hall, Upper Saddle River, New Jersey, 1996.

Thompson, Simon Haskell: The Craft of Functional Programming, International Computer Science Series. Addison-Wesley, Wokingham, England, 1999.

Epp, Susanna S. Discrete Mathematics with ApplicationsComputer Science Press, New York, 1995.

Bergmann, Merrie The Logic Book, McGraw-Hill.

Munro, John Discrete Mathematics for Computing Thomas Nelson.