Software Eng. 2FO4 - Applications of Mathematical Logic in Software Engineering

INSTRUCTOR:

Dr. Mark Lawford

Office: JHE 302/C; Phone: Ext. 24911; E-mail: lawford@McMaster. CA

Tentative Office Hours: Friday 14:30-16:30

LECTURES:

• Location: BSB/304

• Time: Tuesday, Thursday & Friday 11:30-12:20

LABS:

• Location: ABB-273 and ABB-274

• Time: Thursdays 14:30-17:20

MISSION:

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 analyze 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.

OBJECTIVES:

The student will learn to use mathematical logic to describe properties of program states and to verify program properties. Students will learn to about at least two mathematical logic support systems.

GRADING:¹

• Midterm exam (2 hours) 25%

• Assignments/Labs 15%

• Final exam (3 hours) 60%

TEXTS:

1.  Jean E. Rubin, Mathematical Logic: Applications and Theory, Saunders College Publishing, 1990.

2.  SFWR ENG 2F04 Course Pack

ADDITIONAL REFERENCES:

• Course Webpage: http://www.cas.mcmaster.ca/~lawford/2F04/

• W. K. Grassmann and Jean-Paul Tremblay, Logic and Discrete Mathematics: A Computer Science Perspective, Prentice-Hall, 1996.

• Michael R. A. Huth and Mark D. Ryan, Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press, 2000.

DETAILED COURSE OUTLINE:

Why we need logic in software (and hardware) design : (1 hours) (slides: pdf or postscript)

• Problems in writing and checking specifications

• Problems in program documentation and inspection

• Examples: Pentium floating point bug, safety critical software - reactor shutdown systems

Propositional Logic : (5 hours) (slides: pdf or postscript)

• Notation, truth tables

• Tautologies

• Logical equivalence, logical implication - Applications: Circuit simplification and “Building the world with NAND”

• Normal forms (DNF, CNF) - Application: Minimizing gate delays

• Axioms, rules of inference (slides: pdf or postscript)

• Deduction, resolution, duality

• Valid arguments and rules of inference, consistent assumptions

• Use of propositional logic to describe program states.

• Sequent calculus & Propositional reasoning in PVS (slides: pdf or postscript)

Predicate Logic : (8 hours) (slides: pdf or postscript)

• First-order quantification

• Interpretations, models, and validity - tautologies involving quantifiers

• Proofs by predicate logic from premises and inference rules (slides: pdf or postscript)

• Predicate logic with equality (slides: pdf or postscript)

• Use of Predicate logic to describe program states

• Proving program properties in PVS (slides: pdf or postscript)

• Higher Order Logic

The problem of partial functions and non-denoting terms in logic : (1 hour) (slides: pdf or postscript)

Types : (5 hours) (slides: pdf or postscript)

• Ill-defined sets and paradoxes - Liar's paradox, Russell's paradox

• Sets, sorts, types and signatures

• Subtypes and dependent types

• Type checking

• Type checking in PVS

• Tabular specifications in PVS (slides for Power Conditioning example: pdf or postscript)

Mathematical Induction : (5 hour) (slides: pdf or postscript)

• inductive definitions

• weak and strong induction

• proof by induction in PVS and IMPS

Other theorem provers: IMPS : (2 hours) (slides: pdf or postscript)

• Comparison of IMPS and PVS

• Untyped and strongly typed logics

• Treatment of undefined terms

• Comparison of little theories and big theory styles

Introduction to completeness, soundness and other issues : (2 hours)

• Overview of completeness, soundness and decidability results for propositional and predicate logic

• Complexity of decision procedures

• Expressive power of logics

Survey of other types of logics : (4 hours)

• Equational logic

• Intuitionist logic

• Multiple valued logics

• Temporal logics LTL and CTL

Model checking : (3 hours)

• Review of models

• Model Checking

• Verification of program safety and liveness properties

• Model checking with PVS and other tools

NOTES:

Discrimination

“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

“Students are reminded that they should read and comply with the Statements on Academic Ethics and the Senate Resolutions on Academic Dishonesty as found in the Senate Policy Statements distributed at registrations and available in the Senate Office.”

Calculators

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.