In formal methods, program refinement is the 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 sets for example) into implementable data structures.

PropertyValue
dbpprop:abstract
  • In formal methods, program refinement is the 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 sets for example) into implementable data structures. Operation refinement converts a specification of an operation on a system into an implementable program. 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. Retrenchment is an alternative technique when formal refinement is not possible. The opposite of refinement is abstraction. Refinement calculus is one method for program refinement. The FermaT Transformation System is an industrial-strength implementation of refinement.
  • En informatique, le raffinement consiste à avoir une approche de conception où on affine à chaque étape le niveau de détails; le but étant d'atteindre le niveau de granularité. On appelle aussi cette approche, « approche descendante ».
  • 詳細化（しょうさいか、Refinement）とは、形式手法において、抽象的な形式仕様記述から具体的な実行プログラムへと検証可能な変換を行うことである。
dbpprop:hasPhotoCollection
rdf:type
rdfs:comment
  • In formal methods, program refinement is the 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 sets for example) into implementable data structures.
  • En informatique, le raffinement consiste à avoir une approche de conception où on affine à chaque étape le niveau de détails; le but étant d'atteindre le niveau de granularité. On appelle aussi cette approche, « approche descendante ».
  • 詳細化（しょうさいか、Refinement）とは、形式手法において、抽象的な形式仕様記述から具体的な実行プログラムへと検証可能な変換を行うことである。
rdfs:label
  • Program refinement
  • Raffinement
  • 詳細化
owl:sameAs
skos:subject
foaf:page
is dbpprop:disambiguates of
is dbpprop:redirect of
is owl:sameAs of