# Program refinement

Program refinement
Data transformation/Source transformation
Concepts
metadata · data mapping
data transformation · model transf.
Languages
ATL · AWK · MOFM2T · QVT · TXL
XML languages
Techniques and transforms
identity · synthesis · refinement
Applications
data migration · data conversion
ETL · program transformation
Application fields
Data warehouse
Software engineering
Software languages: macro, preprocessing, template

In formal methods, program refinement is the verifiable transformation of an abstract (high-level) formal specification into a concrete (low-level) executable program.[citation needed] Stepwise refinement allows this process to be done in stages. Logically, refinement normally involves implication, but there can be additional complications.

## Data refinement

Data refinement is used to convert an abstract data model (in terms of sets for example) into implementable data structures (such as arrays).[citation needed] Operation refinement converts a specification of an operation on a system into an implementable program (e.g., a procedure). The postcondition can be strengthened and/or the precondition weakened in this process. This reduces any nondeterminism in the specification, typically to a completely deterministic implementation.

For example, x ∈ {1,2,3} (where x is the value of the variable x after an operation) could be refined to x ∈ {1,2}, then x ∈ {1}, and implemented as x := 1. Implementations of x := 2 and x := 3 would be equally acceptable in this case, using a different route for the refinement. However, we must be careful not to refine to x ∈ {} (equivalent to false) since this is unimplementable; it is impossible to select a member from the empty set.

The term reification is also sometimes used (coined by Cliff Jones). Retrenchment is an alternative technique when formal refinement is not possible. The opposite of refinement is abstraction.

## Algorithm refinement

Refinement calculus is a formal system (inspired from Hoare logic) that promotes program refinement. The FermaT Transformation System is an industrial-strength implementation of refinement. B-Method is also a Formal method that extends refinement calculus with a component language: it has been used in industrial developments.

In type theory, a refinement type[1][2][3] is a type endowed with a predicate which is assumed to hold for any element of the refined type. Refinement types can express preconditions when used as function arguments or postconditions when used as return types: for instance, the type of a function which accepts natural numbers and returns natural numbers greater than 5 may be written as $f: \mathbb{N} \rarr \{n: \mathbb{N} | n > 5\}$. Refinement types are thus related to behavioral subtyping.

## References

1. ^ Freeman, T.; Pfenning, F. (1991). "Reﬁnement types for ML". Proceedings of the ACM Conference on Programming Language Design and Implementation. pp. 268–277.
2. ^ Hayashi, S. (1993). "Logic of reﬁnement types". Proceedings of the Workshop on Types for Proofs and Programs. pp. 157–172.
3. ^ Denney, E. (1998). "Reﬁnement types for speciﬁcation". Proceedings of the IFIP International Conference on Programming Concepts and Methods. 125. Chapman & Hall. pp. 148–166.

Wikimedia Foundation. 2010.

Нужно решить контрольную?

### Look at other dictionaries:

• Refinement calculus — is a formalized approach to stepwise refinement for program construction. The required behaviour of the final executable program is specified as an abstract and perhaps non executable program , which is then refined by a series of correctness… …   Wikipedia

• Refinement — may refer to:* Equilibrium refinement, the identification of actualized equilibria in game theory * Program refinement, the verifiable transformation of a formal specification into source code which can be compiled into an executable program *… …   Wikipedia

• Program transformation — A program transformation is any operation that takes a program and generates another program. It is often important that the derived program be semantically equivalent to the original, relative to a particular formal semantics. Other program… …   Wikipedia

• Program derivation — In computer science, program derivation is the derivation of a program from its specification, by mathematical means.To derive a program means to write a formal specification, which is usually non executable, and then apply mathematically correct …   Wikipedia

• Coot (program) — Coot the Coot main window (version 0.5pre) Developer(s) …   Wikipedia

• Rietveld refinement — is a technique devised by Hugo Rietveld for use in the characterisation of crystalline materials. The neutron and x ray diffraction of powder samples results in a pattern characterised by peaks in intensity at certain positions. The height, width …   Wikipedia

• Medicaid Drug Rebate Program — The Medicaid Drug Rebate Program is a program in the United States that was created by the Omnibus Budget Reconciliation Act of 1990 (OBRA 90). It requires that drug manufacturers have a national rebate agreement with the Secretary of the… …   Wikipedia

• Medicaid Drug Debate Program — The Medicaid Drug Rebate Program is a program in the United States that was created by the Omnibus Budget Reconciliation Act of 1990 (OBRA 90). It requires that drug manufacturers have a national rebate agreement with the Secretary of the… …   Wikipedia

• ECL programming language — The ECL programming language and system was an extensible high level programming language and development environment developed at Harvard University in the 1970s. The name ECL stood for Extensible Computer Language or EClectic Language . Some… …   Wikipedia

• Design by contract — (DbC) or Programming by Contract is an approach to designing computer software. It prescribes that software designers should define formal, precise and verifiable interface specifications for software components, which extend the ordinary… …   Wikipedia