 | This articleneeds additional citations forverification. Please helpimprove this article byadding citations to reliable sources. Unsourced material may be challenged and removed. Find sources: "Refinement" computing – news ·newspapers ·books ·scholar ·JSTOR(September 2010) (Learn how and when to remove this message) |
| Data transformation |
|---|
| Concepts |
| Transformation languages |
| Techniques and transforms |
| Applications |
| Related |
Refinement is a generic term of computer science that encompasses various approaches for producingcorrect computer programs and simplifying existing programs to enable their formal verification.
Informal methods,program refinement is theverifiable transformation of anabstract (high-level)formal specification into aconcrete (low-level)executable program.[citation needed]Stepwise refinement allows this process to be done in stages. Logically, refinement normally involvesimplication, but there can be additional complications.
The progressive just-in-time preparation of the product backlog (requirements list) inagile software development approaches, such asScrum, is also commonly described as refinement.[1]
Data refinement is used to convert an abstract data model (in terms ofsets for example) into implementabledata structures (such asarrays).[citation needed] Operation refinement converts aspecification of an operation on a system into an implementableprogram (e.g., aprocedure). Thepostcondition can be strengthened and/or theprecondition weakened in this process. This reduces anynondeterminism in the specification, typically to a completelydeterministic implementation.
For example,x ∈ {1,2,3} (wherex is the value of thevariablex after an operation) could be refined tox ∈ {1,2}, thenx ∈ {1}, and implemented asx := 1. Implementations ofx := 2 andx := 3 would be equally acceptable in this case, using a different route for the refinement. However, we must be careful not to refine tox ∈ {} (equivalent tofalse) since this is unimplementable; it is impossible to select amember from theempty set.
The termreification is also sometimes used (coined byCliff Jones).Retrenchment is an alternative technique when formal refinement is not possible. The opposite of refinement isabstraction.
Refinement calculus is aformal system (inspired fromHoare logic) that promotes program refinement. TheFermaT Transformation System is an industrial-strength implementation of refinement. TheB-Method is also aformal method that extends refinement calculus with a component language: it has been used in industrial developments.
Intype theory, arefinement type[2][3][4] is a type endowed with a predicate which is assumed to hold for any element of the refined type. Refinement types can expresspreconditions when used asfunction arguments orpostconditions when used asreturn types: for instance, the type of a function which accepts natural numbers and returns natural numbers greater than 5 may be written as. Refinement types are thus related tobehavioral subtyping.
 | Thissoftware-engineering-related article is astub. You can help Wikipedia byexpanding it. |