Lecturer: Zhiming Liu
Aims and Objectives:
This course is to establish a good theoretical understanding of how to describe what programs do, how they do it, and why they work learn how to apply this understanding to the construction and analysis of programs. It about disciplines of programming to ensure the correctness of a program and focus on the problems of
-- How to describe what program do, or define the correctness criteria of programs: specification and abstraction
-- How do they do it: semantics of programs
-- Why they do it: verification of the correctness criteria of a program
-- How to develop a program to ensure the correctness: refinement, synthesis
Syllabus:
Part I. The Mathematical Preparation
-- Complete partial orders (CPO)
-- Complete lattice
-- Propositional and Predicate Calculi
Part II. Understanding the Essence of Computations
- Computation as a change of states
-- Programs as relations on states
Part III: Relational Methods of Imperative Sequential Programming
-- Deterministic and terminating programs as functions of states
-- Nondeterminism as a means of abstraction and nondeterministic and terminating
programs as relations between states
--- Nonterminating programs and upward closure property
-- Program specification in Hoare Logic
-- Programs as predicate transformers
-- Relational Calculus and Unifying Theories of Programming
Part IV. Advanced Topics
-- A relational model for object-oriented designs
-- A relational model of concurrent programs and the temporal logic of actions
-- Real-time systems
-- Fault-tolerance
Reading List:
1. Edsger W. Dijkstra (1976): A discipline of programming, Prentice-Hall, INC.
2. David Gries (1981): The science of programming, Springer.
3. C.A.R. Hoare and He Jifeng (1998): Unifying Theories of programming, Prentice Hall.
4. Zhiming Liu and Mathai Joseph (2005): Real-Time and Fault-Tolerant Systems - Specification,
Verification, Refinement and Scheduling. Technical Report 323, UNU-IIST, P.O.Box 3058 , Macao (http://www.iist.unu.edu/).
5. He Jifeng, Xiaoshan Li (2005): He Jifeng, Xiaoshan Li, and Zhiming Liu. A Refinement Calculus for Object Systems. Technical Report 322, UNU-IIST, P.O.Box 3058, Macau (http://www.iist.unu.edu/).