Refinement calculus
It is proposed that this article be deleted because of the following concern:
If you can address this concern by improving, copyediting, sourcing, renaming, or merging the page, please edit this page and do so. You may remove this message if you improve the article or otherwise object to deletion for any reason. Although not required, you are encouraged to explain why you object to the deletion, either in your edit summary or on the talk page. If this template is removed, do not replace it. This message has remained in place for seven days, so the article may be deleted without further notice. Find sources: "Refinement calculus" – news · newspapers · books · scholar · JSTOR Nominator: Please consider notifying the author/project: {{subst:proposed deletion notify|Refinement calculus|concern=Appears to be a very obscure program/technology/calculus, no news on it from any major publications, one of the two reference is a dead link, the second reference is a primary source providing little information.}} ~~~~Timestamp: 20220526094917 09:49, 26 May 2022 (UTC) Administrators: delete |
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 series of correctness-preserving transformations into an efficiently executable program.[1]
Proponents include Ralph-Johan Back, who originated the approach in his 1978 PhD thesis On the Correctness of Refinement Steps in Program Development, and Carroll Morgan, especially with his book 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 specification statements as pre- and postconditions standing, on their own, for any program that could soundly be placed between them.
References
- ^ Butler, Michael. "Refinement Calculus Tutorial". Retrieved 22 April 2020.
External links
 | This formal methods-related article is a stub. You can help Wikipedia by expanding it. |