SE 212: Logic and Computation

• Announcements

General

• Course Description

Calendar Description

SE212
Logic and Computation
Formal logic. Proof systems and styles. Rudimentary model theory. Logic-based specification. Correctness proofs. Applications in software engineering.

Course Goals

This course is about the "first principles" of the logical theory behind software engineering. Students will be introduced to logical notation (both propositional and predicate logic), and basic methods of proof. Specification and program correctness are the main applications of logic taught in this course. This course teaches "verification in the small", i.e., reasoning about statements within an individual function. Students will acquire reasoning skills, understand the meaning of programs in a formal way, and learn how verification is necessary to expose subtle flaws.

At the end of this course, a student should:

1. be able to read and write logical statements in propositional and predicate logic.
2. be able to prove theorems in propositional and predicate logic.
3. know there are multiple ways to prove these theorems.
4. be able to express desired program behaviour in logic.
5. understand the idea of program correctness.
6. be able to verify formally that functions within a program are correct (verification in the small).
7. understand the difference between testing, inspection, and formal verification.
8. understand there is a mathematical theory associated with software engineering.