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. This reduces any nondeterminism in the specification, typically to a completely deterministic implementation.
For example, x ∈ {1,2,3} (where x is the value of the 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 member from the empty set.
The term reification is also sometimes used (coined by Cliff Jones). Retrenchment is an alternative technique when formal refinement is not possible. The opposite of refinement is abstraction.
Read more about this topic: Refinement (computing)
Famous quotes containing the words data and/or refinement:
“To write it, it took three months; to conceive it three minutes; to collect the data in it—all my life.”
—F. Scott Fitzgerald (1896–1940)
“You know that your toddler needed love and approval but he often seemed not to care whether he got it or not and never seemed to know how to earn it. Your pre-school child is positively asking you to tell him what does and does not earn approval, so he is ready to learn any social refinement of being human which you will teach him....He knows now that he wants your love and he has learned how to ask for it.”
—Penelope Leach (20th century)