Refinement (computing): Difference between revisions

Revision as of 17:09, 22 July 2015

Revision as of 11:47, 11 April 2016

Line 9:

== 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]]).{{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.

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