# Refinement (computing)

> Mediated Wiki article. Canonical URL: https://mediated.wiki/source/Refinement_(computing)
> Markdown URL: https://mediated.wiki/source/Refinement_(computing).md
> Source: https://en.wikipedia.org/wiki/Refinement_(computing)
> Source revision: 1215731572
> License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/)

This article needs additional citations for verification. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed. Find sources: "Refinement" computing – news · newspapers · books · scholar · JSTOR (September 2010) (Learn how and when to remove this message)

Data transformation Concepts Metadata Data element Data mapping Data migration Data transformation Model transformation Macro Preprocessor Transformation languages ATL AWK MOFM2T QVT XML languages Techniques and transforms Identity transform Data refinement Applications Data conversion Data migration Data integration Extract, transform, load (ETL) Web template system Related Data wrangling Transformation languages v t e

**Refinement** is a generic term of computer science that encompasses various approaches for producing [correct](/source/Correctness_(computer_science)) computer programs and simplifying existing programs to enable their formal verification.

## Program refinement

In [formal methods](/source/Formal_methods), **program refinement** is the [verifiable](/source/Formal_verification) transformation of an *abstract* (high-level) [formal specification](/source/Formal_specification) into a *concrete* (low-level) [executable program](/source/Executable_program).[*[citation needed](https://en.wikipedia.org/wiki/Wikipedia:Citation_needed)*] *[Stepwise refinement](/source/Stepwise_refinement)* allows this process to be done in stages. Logically, refinement normally involves [implication](/source/Logical_consequence), but there can be additional complications.

The progressive just-in-time preparation of the product backlog (requirements list) in [agile software development](/source/Agile_software_development) approaches, such as [Scrum](/source/Scrum_(software_development)), is also commonly described as refinement.[1]

## Data refinement

**Data refinement** is used to convert an abstract data model (in terms of [sets](/source/Set_(mathematics)) for example) into implementable [data structures](/source/Data_structures) (such as [arrays](/source/Array_data_structure)).[*[citation needed](https://en.wikipedia.org/wiki/Wikipedia:Citation_needed)*] Operation refinement converts a [specification](/source/Specification) of an operation on a system into an implementable [program](/source/Computer_program) (e.g., a [procedure](/source/Procedure_(computer_science))). The [postcondition](/source/Postcondition) can be strengthened and/or the [precondition](/source/Precondition) weakened in this process. This reduces any [nondeterminism](/source/Nondeterministic_algorithm) in the specification, typically to a completely [deterministic](/source/Deterministic) implementation.

For example, *x* ∈ {1,2,3} (where *x* is the value of the [variable](/source/Variable_(programming)) *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](/source/Element_(mathematics)) from the [empty set](/source/Empty_set).

The term [reification](/source/Reification_(computer_science)) is also sometimes used (coined by [Cliff Jones](/source/Cliff_Jones_(computer_scientist))). [Retrenchment](/source/Retrenchment_(computing)) is an alternative technique when formal refinement is not possible. The opposite of refinement is [abstraction](/source/Abstraction_(computer_science)).

## Refinement calculus

[Refinement calculus](/source/Refinement_calculus) is a [formal system](/source/Formal_system) (inspired from [Hoare logic](/source/Hoare_logic)) that promotes program refinement. The [FermaT Transformation System](https://en.wikipedia.org/w/index.php?title=FermaT_Transformation_System&action=edit&redlink=1) is an industrial-strength implementation of refinement. The [B-Method](/source/B-Method) is also a [formal method](/source/Formal_method) that extends refinement calculus with a component language: it has been used in industrial developments.

## Refinement types

Main article: [Refinement type](/source/Refinement_type)

In [type theory](/source/Type_theory), a **refinement type**[2][3][4] is a type endowed with a predicate which is assumed to hold for any element of the refined type. Refinement types can express [preconditions](/source/Precondition) when used as [function arguments](/source/Function_argument) or [postconditions](/source/Postcondition) when used as [return types](/source/Return_type): for instance, the type of a function which accepts natural numbers and returns natural numbers greater than 5 may be written as f : N → { n : N | n > 5 } {\displaystyle f:\mathbb {N} \rightarrow \{n:\mathbb {N} \,|\,n>5\}} . Refinement types are thus related to [behavioral subtyping](/source/Behavioral_subtyping).

## See also

- [Reification (computer science)](/source/Reification_(computer_science))

## References

1. **[^](#cite_ref-1)** Cho, L (2009). "Adopting an Agile Culture a User Experience Team's Journey". *2009 Agile Conference*. pp. 416–421. [doi](/source/Doi_(identifier)):[10.1109/AGILE.2009.76](https://doi.org/10.1109%2FAGILE.2009.76). [ISBN](/source/ISBN_(identifier)) [978-0-7695-3768-9](https://en.wikipedia.org/wiki/Special:BookSources/978-0-7695-3768-9). [S2CID](/source/S2CID_(identifier)) [38580329](https://api.semanticscholar.org/CorpusID:38580329).

1. **[^](#cite_ref-2)** Freeman, T.; Pfenning, F. (1991). ["Refinement types for ML"](https://www.cs.cmu.edu/~fp/papers/pldi91.pdf) (PDF). *Proceedings of the ACM Conference on Programming Language Design and Implementation*. pp. 268–277. [doi](/source/Doi_(identifier)):[10.1145/113445.113468](https://doi.org/10.1145%2F113445.113468).

1. **[^](#cite_ref-3)** Hayashi, S. (1993). "Logic of refinement types". *Proceedings of the Workshop on Types for Proofs and Programs*. pp. 157–172. [CiteSeerX](/source/CiteSeerX_(identifier)) [10.1.1.38.6346](https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.6346). [doi](/source/Doi_(identifier)):[10.1007/3-540-58085-9_74](https://doi.org/10.1007%2F3-540-58085-9_74).

1. **[^](#cite_ref-4)** Denney, E. (1998). "Refinement types for specification". *Proceedings of the IFIP International Conference on Programming Concepts and Methods*. Vol. 125. Chapman & Hall. pp. 148–166. [CiteSeerX](/source/CiteSeerX_(identifier)) [10.1.1.22.4988](https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.4988).

This software-engineering-related article is a stub. You can help Wikipedia by adding missing information.

- [v](https://en.wikipedia.org/wiki/Template:Software-eng-stub)
- [t](/source/Template_talk%3ASoftware-eng-stub)
- [e](https://en.wikipedia.org/wiki/Special:EditPage/Template:Software-eng-stub)

---
Adapted from the Wikipedia article [Refinement (computing)](https://en.wikipedia.org/wiki/Refinement_(computing)) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/Refinement_(computing)?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.