Program refinement
   HOME

TheInfoList



OR:

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. '' 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 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 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 is an industrial-strength implementation of refinement. The B-Method 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 arguments 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 f: \mathbb \rarr \. Refinement types are thus related to behavioral subtyping.


See also

* Reification (computer science)


References

Formal methods terminology Computer programming {{soft-eng-stub