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.

Proponents include Ralph-Johan Back, who originated the approach in his 1978 PhD thesis "On the Correctness of Refinement Steps in Program Development", and [http://www.cse.unsw.edu.au/db/staff/info/carrollm.html Carroll Morgan] , especially with his book " [http://web.comlab.ox.ac.uk/oucl/publications/books/PfS/ Programming from Specifications] " (Prentice Hall, 2nd edition, 1994, ISBN 0-13-123274-6). In the latter case, the motivation was to link Abrial's specification notation Z, via a rigorous relation of behaviour-preserving program refinement, to an executable programming notation based on Dijkstra's language of guarded commands. "Behaviour-preserving" in this case means that any Hoare triple satisfied by a program should also be satisfied by any refinement of it, which notion leads directly to " [http://www.ecs.soton.ac.uk/~mjb/refcalc-tut/home.html#morgan specification statements] " as pre- and postconditions standing, on their own, for any program that could soundly be placed between them.

External links

* [http://www.abo.fi/~backrj/index.php?page=Refinement%20calculus%20all.html Refinement Calculus information]
* [http://www.ecs.soton.ac.uk/~mjb/refcalc-tut/home.html Refinement Calculus tutorial]


Wikimedia Foundation. 2010.

Игры ⚽ Поможем написать курсовую

Look at other dictionaries:

  • Calculus (disambiguation) — Calculus is Latin for pebble, and has a number of meanings in English: In mathematics and computer science Calculus , in its most general sense, is any method or system of calculation. To modern theoreticians the answer to the question what is a… …   Wikipedia

  • Program refinement — Data transformation/Source transformation Concepts metadata · data mapping data transformation · model transf …   Wikipedia

  • Holomorphic functional calculus — In mathematics, holomorphic functional calculus is functional calculus with holomorphic functions. That is to say, given a holomorphic function fnof; of a complex argument z and an operator T , the aim is to construct an operator:f(T),which in a… …   Wikipedia

  • RCOS — is a relational semantic model and refinement calculus for object oriented and component based software development. It was originally developed by He Jifeng, Zhiming Liu and Xiaoshan Li at UNU IIST. It supports both state based and event based… …   Wikipedia

  • List of mathematics articles (R) — NOTOC R R. A. Fisher Lectureship Rabdology Rabin automaton Rabin signature algorithm Rabinovich Fabrikant equations Rabinowitsch trick Racah polynomials Racah W coefficient Racetrack (game) Racks and quandles Radar chart Rademacher complexity… …   Wikipedia

  • Predicate transformer semantics — is an extension of Floyd Hoare Logic invented by Dijkstra and extended and refined by other researchers. It was first introduced in Dijkstra s paper Guarded commands, nondeterminacy and formal derivation of programs . It is a method for defining… …   Wikipedia

  • Слабейшее предусловие — Преобразователи предикатов расширение логики Флойда Хоара, сделанное Э. Дейкстрой. Впервые появившись в [1][1], с помощью этого метода определяется семантика императивного программирования и соответствующего языка. В нём каждой команде языка… …   Википедия

  • Ralph-Johan Back — is a Finnish computer scientist.Back originated the Refinement Calculus, an important approach to the formal development of programs using stepwise refinement, in his 1978 PhD thesis at the University of Helsinki, On the Correctness of Refinement …   Wikipedia

  • Java Modeling Language — The Java Modeling Language (JML) follows the design by contract paradigm. It is a specification language for Java programs, using . There are various verification tools for JML, such as a runtime assertion checker and the Extended Static Checker… …   Wikipedia

  • Michael Butler (computer scientist) — Michael J. Butler is Professor of Computer Science at the University of Southampton, UK. Butler was originally from Ireland and received his Bachelors degree in Computer Science from Trinity College, Dublin in 1988. He then undertook an MSc and… …   Wikipedia

Share the article and excerpts

Direct link
… Do a right-click on the link above
and select “Copy Link”