Software Eng. 2FO3 - Logic For Software Engineering

Dr. Mark Lawford
Office: ITB 160; E-mail:
Tentative Office Hours: Friday 14:30-16:30

Grad: Vera Pantelic (
Office: ITB/205
Undergrad: Emery Finkelstein (




The role of logic in software engineering is much like the role of calculus in other fields. Logical expressions can be used to describe designs and logical analysis used to analyse design documents. This course teaches logic in much the same way that early engineering calculus courses teach calculus. Rather than exploring the fundamental assumptions and methods of logic, this course teaches how logic can be used by the software developer. The course provides basic knowledge of the terminology and notation of the field and stresses applications. Issues that would concern mathematicians and logicians get relatively little time although students will know enough about those issues that they will be able to understand discussions where they are mentioned.


The student will learn to use mathematical logic to describe properties of program states and to verify program properties. Students will be introduces to an automated theorem prover system.


Two marking schemes are provided. In order to have your assignments count in your final mark (Scheme A), you must pass (obtain > 50%) on the combination of your attendance, midterm, & final (Scheme B). Provided you pass by Scheme B, your final mark will be the max(Scheme A, Scheme B).

Scheme A

Midterm exam 20%
Assignments/Quizzes 10%
Final exam 60%

Scheme B

Midterm exam 25%
Assignments/Quizzes 0%
Attendance/Participation 5%
Final exam 70%

NOTE: In order to pass the course you must pass the combination of the midterm and final. Also, a student may miss 4 lectures without an attendance penalty. Additional missed classes incur a -1
2% penalty.




Why we need logic in software (and hardware) design:
(slides: Intro.pdf)
Propositional Logic:
(slides: prop.pdf)
Predicate Logic:
(slides: pred.pdf)
Mathematical Induction:
(slides: induction.pdf)
The problem of partial functions and non-denoting terms in logic:
(slides: partial.pdf)
(slides: type.pdf)
Introduction to completeness, soundness and other issues:
(slides: tba)
Survey of other types of logics:
(slides: tba)
Model checking:
(slides: model.pdf)
Program Verification:
(slides: Verification.pdf)



“The Faculty of Engineering is concerned with ensuring an environment that is free of all adverse discrimination. If there is a problem that cannot be resolved by discussion among the persons concerned individuals are reminded that they should contact there Chair, the Sexual Harassment Office or the Human Rights Consultant, as soon as possible.”

Academic Dishonesty

“Academic dishonesty consists of misrepresentation by deception or by other fraudulent means and can result in serious consequences, e.g. the grade of zero on an assignment, loss of credit with a notation on the transcript (notation reads: ‘Grade of F assigned for academic dishonesty’), and/or suspension or expulsion from the university. It is your responsibility to understand what constitutes academic dishonesty. For information on the various kinds of academic dishonesty please refer to the Academic Integrity Policy, specifically Appendix 3, located at\_integrity.htm
The following illustrates only three forms of academic dishonesty:

  1. Plagiarism, e.g. the submission of work that is not one’s own or for which other credit has been obtained. An example is copying all or part of someone’s assignment and handing it in as your own.
  2. Improper collaboration in group work.
  3. Copying or using unauthorized aids in tests and examinations.”


Calculators are not needed for this course and their use will not be permitted during tests.

Bonus Marks

At the discretion of the instructor, a student will receive 1 to 2 “bonus marks” on their latest assignment for being the first person to point out a technical error in the lecture slides or assignment handout.