Content deleted Content added
unreferenced |
|||
Line 1:
{{unreferenced}}
In [[formal methods]], '''program refinement''' is the [[formal verification|verifiable]] transformation of an ''abstract'' (high-level) [[formal specification]] into a ''concrete'' (low-level) [[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 (mathematics)|set]]s for example) into implementable [[data structures]] (such as [[Array data structure|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. This reduces any [[Nondeterministic algorithm|nondeterminism]] in the specification, typically to a completely [[deterministic]] implementation.
| |||