Downloading: slides

All slides are packaged as zip archives. The HTML archives contain a html file and a gif file for every slide, all stored in a single subdirectory. The PDF archives contain a single PDF file, ready for use.

HTML

  1. Introduction
  2. Propositional Logic
  3. Predicate Logic
  4. Equality and Definite Description
  5. Sets
  6. Definitions
  7. Relations
  8. Functions
  9. Sequences
  10. Free Types
  11. Schemas
  12. Schema Operators
  1. Promotion
  2. Preconditions
  3. A File System
  4. Data Refinement
  5. Data Refinement and Schemas
  6. Functional Refinement
  7. Refinement Calculus
  8. A Telecommunications Protocol
  9. An Operating System Scheduler
  10. A Bounded Buffer Module
  11. A Save Area

Colour PDF

  1. Introduction
  2. Propositional Logic
  3. Predicate Logic
  4. Equality and Definite Description
  5. Sets
  6. Definitions
  7. Relations
  8. Functions
  9. Sequences
  10. Free Types
  11. Schemas
  12. Schema Operators
  1. Promotion
  2. Preconditions
  3. A File System
  4. Data Refinement
  5. Data Refinement and Schemas
  6. Functional Refinement
  7. Refinement Calculus
  8. A Telecommunications Protocol
  9. An Operating System Scheduler
  10. A Bounded Buffer Module
  11. A Save Area

Monochrome PDF (four-up)

  1. Introduction
  2. Propositional Logic
  3. Predicate Logic
  4. Equality and Definite Description
  5. Sets
  6. Definitions
  7. Relations
  8. Functions
  9. Sequences
  10. Free Types
  11. Schemas
  12. Schema Operators
  1. Promotion
  2. Preconditions
  3. A File System
  4. Data Refinement
  5. Data Refinement and Schemas
  6. Functional Refinement
  7. Refinement Calculus
  8. A Telecommunications Protocol
  9. An Operating System Scheduler
  10. A Bounded Buffer Module
  11. A Save Area
text slides exercises solutions cards contents