Refinement (computing): Difference between revisions

Revision as of 18:31, 24 January 2009

Revision as of 19:05, 24 April 2009

Line 1:

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]]. ''[[Stepwise refinement]]'' allows this process to be done in stages. Logically, refinement normally involves [[implication]], but there can be additional complications. ''[[Data refinement]]'' is used to convert an abstract data model (in terms of [[set|sets]]s for example) into implementable [[data structures]] (such as [[Array|arraysarray]]s). ''[[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, <i>''x'</i>'' &isin;∈ {1,2,3} (where <i>''x'</i>'' is the value of the [[Variable (programming)|variable]] <i>''x</i>'' after an operation) could be refined to <i>''x'</i>'' &isin;∈ {1,2}, then <i>''x'</i>'' &isin;∈ {1}, and implemented as <i>''x</i>'' := 1. Implementations of <i>''x</i>'' := 2 and <i>''x</i>'' := 3 would be equally acceptable in this case, using a different route for the refinement. However, we must be careful not to refine to <i>''x'</i>'' &isin;∈ {} (equivalent to <i>''false</i>'') since this is unimplementable; it is impossible to select a [[Element (mathematics)|member]] from the [[empty set]].

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

Line 8:

[[Category:Formal methods]]

{{soft-eng-stub}}