Refinement (computing)

This is an old revision of this page, as edited by Jpbowen (talk | contribs) at 14:47, 31 August 2005 (Added "Data refinement" and "Operation refinement"). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.
(See also selectivity for a non-computer science meaning.)

In formal methods, refinement is the verifiable transformation of an abstract formal specification into a concrete 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 sets for example) into implementable data structures (such as arrays). 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.

The term reification is also sometimes used. Retrenchment is an alternative technique when formal refinement is not possible. The opposite of refinement is abstraction, something that many computer science students find very difficult!