- Author
- Carroll Morgan, Ken Robinson and Paul Gardiner, Oxford University Computing Laboratory
- Published
- October 1988
- Kind
- Technical monograph collecting seven papers and a summary of laws
- Original
- www.cs.ox.ac.uk/files/3391/PRG70.pdf
- Subject
- Formal methods and proof
What it is
The monograph is Technical Monograph PRG-70 of the Oxford Programming Research Group. Carroll Morgan's introduction says it collects only the work done at Oxford. Its aim is a calculus for turning specifications into executable programs.
What it says
- The introduction defines the refinement calculus as notation and rules for deriving programs from specifications. Derivations happen inside one language.
- A specification statement written [pre, post] stands in for code not yet developed. The papers give it a weakest precondition meaning, so it counts as an abstract program.
- The papers introduce miracles, statements that break Dijkstra's law of the excluded miracle. They say miracles simplify derivation, as negative numbers simplify arithmetic.
- Refinement of P by Q means every specification met by P is met by Q.
- Procedure calls are treated as plain text substitution of a body for a name. The same substitution can apply to code or to specifications.
- Data refinement swaps abstract local variables for concrete ones. One paper aims to calculate such refinements rather than prove them after the fact.
- A summary of laws warns that the basic laws alone give very long derivations. Experienced users build more powerful laws to make derivations routine.
What evidence it gives
The papers give formal definitions, laws proved with weakest preconditions, and worked program derivations. Examples include a specification for a square root and one for array search. There are no experiments or user studies.
Interests and limits
Most proofs and derivations were not read; front matter, abstracts and laws were. The PDF text comes from scanned pages and has recognition errors. The authors are the creators of the method they present.