Refinement is a generic term of computer science that encompasses various approaches for producing
correct computer programs and simplifying existing programs to enable their formal verification.
Program refinement
In
formal methods
In computer science, formal methods are mathematics, mathematically rigorous techniques for the formal specification, specification, development, Program analysis, analysis, and formal verification, verification of software and computer hardware, ...
, program refinement is the
verifiable transformation of an ''abstract'' (high-level)
formal specification
In computer science, formal specifications are mathematically based techniques whose purpose is to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verify ...
into a ''concrete'' (low-level)
executable program
In computer science, executable code, an executable file, or an executable program, sometimes simply referred to as an executable or binary, causes a computer "to perform indicated tasks according to encoded instructions", as opposed to a da ...
. ''
Stepwise refinement'' allows this process to be done in stages. Logically, refinement normally involves
implication, but there can be additional complications.
The progressive just-in-time preparation of the product backlog (requirements list) in
agile software development
Agile software development is an umbrella term for approaches to software development, developing software that reflect the values and principles agreed upon by ''The Agile Alliance'', a group of 17 software practitioners, in 2001. As documented ...
approaches, such as
Scrum, is also commonly described as refinement.
Data refinement
Data refinement is used to convert an abstract data model (in terms of
set
Set, The Set, SET or SETS may refer to:
Science, technology, and mathematics Mathematics
*Set (mathematics), a collection of elements
*Category of sets, the category whose objects and morphisms are sets and total functions, respectively
Electro ...
s for example) into implementable
data structures
In computer science, a data structure is a data organization and storage format that is usually chosen for efficient access to data. More precisely, a data structure is a collection of data values, the relationships among them, and the functi ...
(such as
arrays
An array is a systematic arrangement of similar objects, usually in rows and columns.
Things called an array include:
{{TOC right
Music
* In twelve-tone and serial composition, the presentation of simultaneous twelve-tone sets such that the ...
). Operation refinement converts a
specification
A specification often refers to a set of documented requirements to be satisfied by a material, design, product, or service. A specification is often a type of technical standard.
There are different types of technical or engineering specificati ...
of an operation on a system into an implementable
program (e.g., a
procedure). The
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. Postconditions are sometimes tested using assertions w ...
can be strengthened and/or the
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.
If a precondition is violated, the effect of the ...
weakened in this process. This reduces any
nondeterminism in the specification, typically to a completely
deterministic
Determinism is the metaphysical view that all events within the universe (or multiverse) can occur only in one possible way. Deterministic theories throughout the history of philosophy have developed from diverse and sometimes overlapping mo ...
implementation.
For example, ''x'' ∈ (where ''x'' is the value of the
variable ''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
Member may refer to:
* Military jury, referred to as "Members" in military jargon
* Element (mathematics), an object that belongs to a mathematical set
* In object-oriented programming, a member of a class
** Field (computer science), entries in ...
from the
empty set
In mathematics, the empty set or void set is the unique Set (mathematics), set having no Element (mathematics), elements; its size or cardinality (count of elements in a set) is 0, zero. Some axiomatic set theories ensure that the empty set exi ...
.
The term
reification is also sometimes used (coined by
Cliff Jones).
Retrenchment
Retrenchment (, an old form of ''retranchement'', from ''retrancher'', to cut down, cut short) is an act of cutting down or reduction, particularly of public expenditure.
Political usage
The word is familiar in its most general sense from the mot ...
is an alternative technique when formal refinement is not possible. The opposite of refinement is
abstraction
Abstraction is a process where general rules and concepts are derived from the use and classifying of specific examples, literal (reality, real or Abstract and concrete, concrete) signifiers, first principles, or other methods.
"An abstraction" ...
.
Refinement calculus
Refinement calculus The 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 se ...
is a
formal system
A formal system is an abstract structure and formalization of an axiomatic system used for deducing, using rules of inference, theorems from axioms.
In 1921, David Hilbert proposed to use formal systems as the foundation of knowledge in ma ...
(inspired from
Hoare logic
Hoare logic (also known as Floyd–Hoare logic or Hoare rules) is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and l ...
) that promotes program refinement. The
FermaT Transformation System
Pierre de Fermat (; ; 17 August 1601 – 12 January 1665) was a French mathematician who is given credit for early developments that led to infinitesimal calculus, including his technique of adequality. In particular, he is recognized for his d ...
is an industrial-strength implementation of refinement. The
B-Method
The B method is a method of software development based on B, a tool-supported formal method based on an abstract machine notation, used in the development of computer software.
Overview
B was originally developed in the 1980s by Jean-Raymond Abr ...
is also a
formal method
Formal, formality, informal or informality imply the complying with, or not complying with, some set of requirements ( forms, in Ancient Greek). They may refer to:
Dress code and events
* Formal wear, attire for formal events
* Semi-formal att ...
that extends refinement calculus with a component language: it has been used in industrial developments.
Refinement types
In
type theory
In mathematics and theoretical computer science, a type theory is the formal presentation of a specific type system. Type theory is the academic study of type systems.
Some type theories serve as alternatives to set theory as a foundation of ...
, a refinement type
is a type endowed with a predicate which is assumed to hold for any element of the refined type. Refinement types can express
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.
If a precondition is violated, the effect of the ...
s when used as
function argument
In mathematics, an argument of a function is a value provided to obtain the function's result. It is also called an independent variable.
For example, the binary function f(x,y) = x^2 + y^2 has two arguments, x and y, in an ordered pair (x, y). T ...
s or
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. Postconditions are sometimes tested using assertions w ...
s when used as
return 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 to
behavioral subtyping.
See also
*
Reification (computer science)
In computer science, reification is the process by which an abstract idea about a computer program, program is turned into an explicit data model or other object created in a programming language. A computable/addressable object—a ''resource''� ...
References
Formal methods terminology
Computer programming
{{soft-eng-stub