Content deleted Content added
(3 intermediate revisions by 3 users not shown) | |||
Line 1:
{{refimprove|date=September 2010}}▼
{{Data transformation}}
▲{{refimprove|date=September 2010}}
'''Refinement''' is a generic term of computer science that encompasses various approaches for producing [[correctness (computer science)|correct]] computer programs and simplifying existing programs to enable their formal verification.
==
In [[formal methods]], '''program refinement''' is the [[formal verification|verifiable]] transformation of an ''abstract'' (high-level) [[formal specification]] into a ''concrete'' (low-level) [[executable program]].{{citation needed|date=September 2010}} ''[[Stepwise refinement]]'' allows this process to be done in stages. Logically, refinement normally involves [[logical consequence|implication]], but there can be additional complications.
The progressive just-in-time preparation of the product backlog (requirements list) in [[agile software development]] approaches, such as [[Scrum (software development)|Scrum]], is also commonly described as refinement.<ref>{{cite
==
'''Data refinement'''<!-- REDIRECTs HERE--> is used to convert an abstract data model (in terms of [[set (mathematics)|set]]s for example) into implementable [[data structures]] (such as [[Array data structure|arrays]]).{{citation needed|date=September 2010}} Operation refinement converts a [[specification]] of an operation on a system into an implementable [[computer program|program]] (e.g., a [[Procedure (computer science)|procedure]]). The [[postcondition]] can be strengthened and/or the [[precondition]] weakened in this process. This reduces any [[Nondeterministic algorithm|nondeterminism]] in the specification, typically to a completely [[deterministic]] implementation.
Line 17 ⟶ 16:
The term [[Reification (computer science)|reification]] is also sometimes used (coined by [[Cliff Jones (computer scientist)|Cliff Jones]]). [[Retrenchment (computing)|Retrenchment]] is an alternative technique when formal refinement is not possible. The opposite of refinement is [[Abstraction (computer science)|abstraction]].
==
[[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. The [[B-Method]] is also a [[formal method]] that extends refinement calculus with a component language: it has been used in industrial developments.
==
{{Main|Refinement type}}
In [[type theory]], a '''refinement type'''<ref>{{cite conference|first1=T.|last1=Freeman|first2=F.|last2=Pfenning|url=https://www.cs.cmu.edu/~fp/papers/pldi91.pdf|doi=10.1145/113445.113468 |title=Refinement types for ML|
==See also==
* [[Reification (computer science)]]
==
{{reflist}}
[[Category:Formal methods terminology]]
[[Category:Computer programming]]
|