Refinement (computing): Difference between revisions

Revision as of 15:16, 31 October 2012

Latest revision as of 20:07, 26 March 2024

(17 intermediate revisions by 15 users not shown)

Line 1:

{{refimprove|date=September 2010}}

{{Data transformation}}

'''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.

{{refimprove|date=September 2010}}

== Program refinement ==

Refinement is a generic term of computer science that encompasses various approaches for producing 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]].{{factcitation 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 book|last=Cho|first=L|title=2009 Agile Conference|chapter=Adopting an Agile Culture a User Experience Team's Journey|year=2009|doi=10.1109/AGILE.2009.76|isbn=978-0-7695-3768-9|pages=416–421|s2cid=38580329}}</ref>

== Program refinement ==

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]].{{fact|date=September 2010}} ''[[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'''<!-- 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]]).{{factcitation 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.

For example, ''x'' ∈ {1,2,3} (where ''x'' is the value of the [[Variable (programming)|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 [[Element (mathematics)|member]] from the [[empty set]].

Line 15 ⟶ 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 ==

[[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.

== Refinement types ==

{{Main|Refinement type}}

In [[type theory]], a '''refinement type'''<ref>{{cite conference|first1=T.|last1=Freeman|first2=F.|last2=Pfenning|title=Refinement types for ML|booktitle=Proceedings of the ACM Conference on Programming Language Design and Implementation|pages=268–277|year=1991}}</ref><ref>{{cite conference|first=S.|last=Hayashi|title=Logic of refinement types|booktitle=Proceedings of the Workshop on Types for Proofs and Programs|pages=157–172|year=1993}}</ref><ref>{{cite conference|first=E.|last=Denney|title=Refinement types for specification|booktitle=Proceedings of the IFIP International Conference on Programming Concepts and Methods|volume=125|pages=148–166|publisher=Chapman & Hall|year=1998}}</ref> is a type endowed with a predicate which is assumed to hold for any element of the refined type. Refinement types can express [[precondition]]s when used as [[function argument]]s or [[postcondition]]s when used as [[return type]]s: for instance, the type of a function which accepts natural numbers and returns natural numbers greater than 5 may be written as <math>f: \mathbb{N} \rarr \{n: \mathbb{N} | n > 5\}</math>. Refinement types are thus related to [[behavioral subtyping]].

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=RefinementRefinement types for ML|booktitlebook-title=Proceedings of the ACM Conference on Programming Language Design and Implementation|pages=268–277|year=1991}}</ref><ref>{{cite conference|first=S.|last=Hayashi|title=Logic of refinementrefinement types|booktitleciteseerx = 10.1.1.38.6346|doi=10.1007/3-540-58085-9_74|book-title=Proceedings of the Workshop on Types for Proofs and Programs|pages=157–172|year=1993}}</ref><ref>{{cite conference|first=E.|last=Denney|citeseerx = 10.1.1.22.4988|title=RefinementRefinement types for specificationspecification|booktitlebook-title=Proceedings of the IFIP International Conference on Programming Concepts and Methods|volume=125|pages=148–166|publisher=Chapman & Hall|year=1998}}</ref> is a type endowed with a predicate which is assumed to hold for any element of the refined type. Refinement types can express [[precondition]]s when used as [[function argument]]s or [[postcondition]]s when used as [[return type]]s: for instance, the type of a function which accepts natural numbers and returns natural numbers greater than 5 may be written as <math>f: \mathbb{N} \rarr \{n: \mathbb{N} \, | \, n > 5\}</math>. Refinement types are thus related to [[behavioral subtyping]].

== References ==

{{reflist}}

==See also==

{{soft-eng-stub}}

* [[Reification (computer science)]]

== References ==

[[Category:Formal methods]]

{{reflist}}

[[Category:Formal methods terminology]]

[[Category:Computer programming]]

[[fr:Raffinement]]

{{soft-eng-stub}}

[[ja:詳細化]]