- Author
- Michael Butler
- Published
- 16 January 1996
- Kind
- Tutorial landing page, with links to example derivations
- Original
- www.southampton.ac.uk/~mbutler/refcalc-tut/home.html
- Subject
- Formal methods and proof
What it is
Michael Butler prepared the tutorial and the page says it was last updated in 1996. It introduces the refinement calculus for turning abstract specification statements into executable programs. The worked examples sit on linked pages.
What it says
- The page presents the refinement calculus as a formalisation of stepwise refinement of programs.
- The notation P1 [= P2 says P2 correctly implements P1. Because refinement is transitive, a step can be split into smaller steps.
- Specifications are written as abstract programs, usually specification statements. One example assigns x an arbitrary element of a non-empty set S.
- The tutorial's example derivations target a Pascal-like subset. They cover swapping, maximum, factorial and searching.
- The notation follows Back and Morris more than Morgan, with minor differences. The page points to Morgan's book for more laws.
What evidence it gives
The page gives definitions, a transitivity rule and one small specification example. It lists eight references. The derivations that would show the method at work are on separate pages.
Interests and limits
Only the landing page was read, not the linked derivations or notation pages. The page is old and brief. It offers no tests of the method. It mentions a prototype tool from a group in Finland.