Formal Methods in Software Engineering COMP2600
Course overview
Course description
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.
Rationale
When software is properly engineered, the processes of analysis, design, evaluation and certification must be rigorous. Errors that arise from imprecision or ambiguity in the specification of a software product must be avoided; similarly the languages and tools used in implementation must be meticulously defined so that designers and implementors are never confused. Lastly, the implementation of the software product must be clearly shown to meet the requirements listed in its specification.
The education of a professional software engineer must include an introduction to the formal notations and techniques so that he/she appreciates that there are situations where the extra precision and rigour of formal notations are needed in some phases of a product's life cycle.
Ideas
This course will carry the main responsibility for teaching:
- the importance of logic, set theory, functions and relations as notations for expressing, in a compact and rigorous way, the things we often want to say about computational objects,
- the notion that inductive definition of data types as sets leads naturally to recursive definition of operations on those types and to structural induction principles,
- basic concepts and notations appropriate to capturing the meanings of programming languages (Hoare logic and weakest precondition calculus),
- some basic techniques for proving properties of programs (particularly partial and total correctness),
- the principles of formal language theory and the relationship between languages and computing machines (regular languages, finite state automata, context free languages),
- the idea that formal notations are manipulable in a way that makes arguments mechanically checkable,
- the concept of logic programming,
- the idea that logic and set theory can be embedded in a notation that is adequate for specifying systems.
The course shares responsibility for teaching software design by developing some of the basic ideas in this area (formal notations for specification, design by contract, verification).
Topics
The following topics will be briefly reviewed:
- basic set theory
- functions and relations as sets
- propositional logic
The following topics will be covered:
- inductive definitions of data types such as numerals, lists, and trees
- recursive definitions of functions
- lambda-calculus notation
- induction as a means to verify recursively defined functions
- parse trees and elementary recursive-descent parsing
- regular expressions and regular languages
- non-deterministic and deterministic finite automata
- context-free grammars and EBNF notation
- predicate calculus notation and basic proof theory
- a specification language based on the predicate calculus
- proving partial correctness
- weakest preconditions and loop invariants
- proving termination
- using functions and logic as executable specification languages
- proof mechanisms: substitutions, unification, and backtracking
- the specification language, Z
- the logic programming language, Prolog
- simple computability theory
- introduction to complexity
Technical skills
A student who succeeds in this course will be able to:
- Work at a simple level with a functional language;
Assessment
The following assessment modes will be used.
final examination All objectives are assessed.
mid-semester examination Objectives 1-4 are assessed.
regular written assignments Collectively, all objectives are assessed.
Textbooks
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.
Workload
Thirty one-hour lectures, eight one-hour tutorials and four two-hour laboratory sessions.
