Laws of data refinement (Q1113664)

The underlying philosophy of the method is that there is no semantic distinction between specifications and programs. A specification notation has more expressive statements and richer data types that are expensive or even impossible to implement. The programming language is the implementable subset of the specification language. Data refinement is viewed as systematic piecewise replacement of more sophisticated data types with simpler types. A new formal definition of data refinement is given and a set of laws is derived.