I. Introduction
 A. Who
 B. motivation for refinement calculus (course spec)
------------------------------------------
        WHY REFINEMENT CALCULUS?

Proving programs correct is
 - important
     + safety critical systems
     + business critical systems
     + teaching, research
 - impossible, in general

Open problems:
 - reasoning about higher-order code
    + procedural abstractions
    + callbacks
 - reasoning about concurrency
 - reasoning about OOP, AOP
 - reasoning about components
 - reasoning about maintenance,
      improvement, optimization

Wide spectrum language
  - specifications and
  - programs

Want "lightweight" formalisms
  - elegant theory
  - easy for programmers to understand

------------------------------------------
  1. more abstract semantic technique
  2. more easily applied
  3. it's new for me
     what about the material interests you?
 C. Plan of course (syllabus)
	Would you make any changes to the plan?
 D. Objectives
  1. meta
                What kind of questions should you be asking?
  2. normal
------------------------------------------
        OBJECTIVES

- Explain the goals of the refinement
  calculus
- How to use it in semantics
- Its advantages, disadvantages, limits

- Judge and improve the quality
  of refinement calculus semantics

- Explain and generalize the its ideas
  from sequential and nondeterministic
  programs
     
- Use the refinement calculus to calculate
  correct implementations
------------------------------------------
 E. How I'll run the course
  1. overview
	would you like to work on some kind of term project like these?
  2. red tape
 F. summary
	any other questions about the course?
II. Semantics Overview
 A. Semantic description techniques
	what does a denotational semantics tell you about a statement?
	an operational semantics?
	an axiomatic semantics?
	---------------------
	{ x >= 3 }
	x := x + 1
	{ x > 3 }
	---------------------
        ---------------------
        (x >= 3) = wp.(x := x+1).(x > 3)
        ---------------------
 B. remark about models, presentations, and theories
	What's the theory that a denotational semantics constructs
		a model for?