Content deleted Content added
mNo edit summary |
mNo edit summary |
||
Line 3:
In [[formal methods]], '''refinement''' is the [[formal verification|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 [[set|sets]] for example) into implementable [[data structures]] (such as [[Array|arrays]]). ''[[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.
The term [[Reification#Alternative uses|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]]
| |||