3 Semester Credit Hours

Course Description

The course begins by introducing (or reviewing) the basic logic that will be used in the course as an aid to programming.  Then we look at formal specifications, and how they are refined to become programs.  At each refinement step, there is a small theorem to be proven (that the step is correct), so that at the end, the program is correct.  Most of the course uses just those programming constructs that are common to most programming languages (assignment statement, if statement, array);  we will also look at parallel and interacting processes briefly, and maybe also at probabilistic programming.  Along the way, we define the formal semantics of the language features we use (both execution control and data structures).  The emphasis is on program development to meet specifications, and on program modifications that preserve correctness, rather than on verification after a program is finished.

Prerequisites

Familiarity with basic boolean algebra / logic (nothing advanced is needed)

Intermediate level programming experience, in any language, including an understanding of recursion

Course Objectives

On successful completion of this course, a student should be able to:

- write formal specifications for computations

- write formal specifications for data types and structures

- refine specifications to program code

- prove that refinements are done correctly

- read and understand the formal semantics of programming language features, including concurrency and interaction

- prove that programs meet specifications

- perform program modifications in a provably safe way

- perform data transformations (replacing one data space with another) in a provably safe way

- formally specify time and space constraints

- prove that time and space constraints are met

- write probabilistic specifications

- prove that computations satisfy probability distributions

- understand programs mathematically

Course Topics

The following topics will be covered in the order shown.

- Introduction to Formal Methods of Software Engineering- Boolean Theory- Boolean Theory continued, Number Theory, Character Theory- Collections: Bunches and Sets- Sequences: Strings and Lists- Functions- Quantifiers- Function Fine Points- Specification- Refinement- Program Development- Time Calculation- Searching- Two Great Examples: Fast Exponentiation and Fibonacci- Space Calculation- Scope and Data Structures- Control Structures - Mid Course Review - Time and Space Dependence and Assertions

- Probabilistic Programming

- Subprograms and Aliasing

- Functional Programming - Recursive Data definition - Recursive Program Definition - Data Theory Design - Program Theory Design - Data Transformation - Limited Queue - Independent Composition (Concurrency) - Sequential to Parallel Transformation - Interactive Variables - Communication Channels - Communication Channels continued

- Final Review

Technical Requirements

No software is required for this course, but a good word processor is helpful for developing and presenting solutions to assignments.

Textbook

Required: Hehner, Eric.  A Practical Theory of Programming. current edition available free online at www.cs.utoronto.ca/~hehner/aPToP.

Additional Reading:

Required: Hoare, C.A.R., Misra, J. Verified Software: Theories, Tools, Experiments, www.cs.utoronto.ca/~hehner/vstte-hoare-misra.pdf.

Disclaimer: The course syllabus may differ slightly from this.  Course descriptions will be provided in your online course. Textbook information is provided only to give more information about the course.  Do Not use this information to purchase a textbook.  Up-to-date information will be provided when you register.