Refinement

	Email		Print
	Bookmark		Link

Refinement

In formal methods

Formal methods

In computer science and software engineering, formal methods are particular kind of mathematically-based techniques for the formal specification, development and formal verification of software and hardware systems....
, program refinement is the verifiable

Formal verification

In the context of hardware and software systems, formal verification is the act of Mathematical proof or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics....
transformation of an abstract (high-level) formal specification

Formal specification

In computer science, a formal specification is a mathematics description of software or hardware that may be used to develop an implementation. It describes what the system should do, not how the system should do it....
into a concrete (low-level) executable program. Stepwise refinement allows this process to be done in stages. Logically, refinement normally involves implication

Implication

Implication may refer to:In logic:* Logical implication, in mathematical logic* Material conditional, in philosophical logicIn linguistics:...
, but there can be additional complications. Data refinement is used to convert an abstract data model (in terms of sets

Set

A set is a collection of distinct objects, considered as an object in its own right. Sets are one of the most fundamental concepts in mathematics....
for example) into implementable data structures (such as arrays

Array

In computer science, an array is a data structure consisting of a group of element s that are accessed by index . In most programming languages each element has the same data type and the array occupies a contiguous area of computer memory....
).

Discussion

Ask a question about 'Refinement'

Start a new discussion about 'Refinement'

Answer questions from other users

Full Discussion Forum

Encyclopedia

In formal methods

Formal methods

Formal verification

Formal specification

Implication

Set

Array

Computer program

Computer programs are Instruction for a computer. A computer requires programs to function. Moreover, a computer program does not run unless its instructions are executed by a Central processing unit; however, a program may communicate an Algorithm#Formalization of algorithms to people without running....
(e.g., a procedure). The postcondition

Postcondition

In computer programming, a postcondition is a condition or Predicate that must always be true just after the execution of some section of code or after an operation in a formal specification....
can be strengthened and/or the precondition

Precondition

In computer programming, a precondition is a condition or Predicate that must always be true just prior to the execution of some section of code or before an operation in a formal specification....
weakened in this process. This reduces any nondeterminism

Nondeterministic algorithm

In computer science, a nondeterminism algorithm is an algorithm with one or more choice points where multiple different Continuation are possible, without any specification of which one will be taken....
in the specification, typically to a completely deterministic implementation.

For example, x' ∈ (where x' is the value of the variable

Variable

A variable is a symbol that stands for a value that may vary; the term usually occurs in opposition to constant, which is a symbol for a non-varying value, i.e....
x after an operation) could be refined to x' ∈ , then x' ∈ , 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

Element (mathematics)

In mathematics, an element or member of a Set is any one of the distinct objects that make up that set....
from the empty set

Empty set

In mathematics, and more specifically set theory, the empty set is the unique Set having no members. Some axiomatic set theories assure that the empty set exists by including an axiom of empty set; in other theories, its existence can be deduced....
.

The term reification

Reification (computer science)

Reification is a process through which a computable/addressable object - a resource - is created in a system, as a proxy for a non computable/addressable object....
is also sometimes used (coined by Cliff Jones). Retrenchment

Retrenchment (computing)

Retrenchment is a technique associated with Formal Methods that was introduced to address some of the perceived limitations of formal, model based refinement, for situations in which refinement might be regarded as desirable in principle, but turned out to be unusable, or nearly unusable, in practice....
is an alternative technique when formal refinement is not possible. The opposite of refinement is abstraction

Abstraction (computer science)

In computer science, abstraction is a mechanism and practice to reduce and factor out details so that one can focus on a few concepts at a time....
.

Refinement calculus

Refinement Calculus

Refinement calculus is a formalized approach to stepwise refinement for program construction. The required behaviour of the final executable program is specified as an abstract and perhaps non-executable "program", which is then refined by a series of correctness-preserving transformations into an efficiently executable program....
is one method for program refinement. The FermaT Transformation System

FermaT Transformation System

The FermaT Transformation System is an industrial strength programtransformation system targeted at reverse engineering, program comprehension...
is an industrial-strength implementation of refinement.