Abstract
This paper describes a calculus for the stepwise and piecewise refinement of expressions. It provides a means for the derivation of executable expressions from initial specifications. We take the view that a refinement calculus consists of: a specification language, which usually includes constructs which are non-executable, but is a "superlanguage " of a programming language; a refinement relation between specifications, which possesses particular properties necessary for the refinement of specifications in a stepwise and piecewise manner; and a set of laws determining how such refinements may proceed.
| Original language | Undefined/Unknown |
|---|---|
| Type | Technical Report |
| Publication status | Published - 1999 |
Cite this
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver