Refinement (computing): Difference between revisions

Revision as of 18:09, 11 March 2006

Revision as of 15:41, 19 June 2006

Line 5:

For example, <i>x'</i> &isin; {1,2,3} (where <i>x'</i> is the value of the [[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 [[member]] from the [[empty set]].

The term [[Reification (computer science)|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 (computer science)|abstraction]], something that many computer science students find very difficult!.

[[Category:Formal methods]]

[[Category:Software engineering]]