A Tool for Developing Correct Programs by Refinement

The refinement calculus for the development of programs from specifications is well suited to mechanised support. We review the requirements for tool support of refinement as gleaned from our experience with a number of existing refinement tools, and report on the design and implementation of a new tool to support refinement based on these requirements. Themain features of the newtool are close integration of refinementand proof in a single tool (the samemechanism is used for both), good management of the refinement context, an extensible theory base that allows the tool to be adapted to new application domains, and a flexible user interface.

Content

Author and article information

Contributors

D. Carrington

I. Hayes

R. Nickson

G. Watson

J. Welsh

Conference

Publication date: July 1996

Publication date (Print): July 1996

Pages: 1-19

Affiliations

[0001]Software Verification Research Centre

Department of Computer Science

The University of Queensland

Queensland 4072, Australia

Article

DOI: 10.14236/ewic/RW1996.3

SO-VID: f3d35d8d-bcf7-497b-ba9a-8845e777d56b

Copyright statement: © D. Carrington et al. Published by BCS Learning and Development Ltd. Proceedings of the BCS-FACS 7th Refinement Workshop, Bath

License:

This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

Conference name: Proceedings of the BCS-FACS 7th Refinement Workshop

Conference acronym: RW

Conference number: 7

Conference location: Bath

Conference date: 3-5 July 1996

Conference sponsor: Electronic Workshops in Computing (eWiC)

Conference theme: BCS-FACS 7th Refinement Workshop

Product

Product Information: 1477-9358BCS Learning & Development

Self URI (article page): https://www.scienceopen.com/hosted-document?doi=10.14236/ewic/RW1996.3

Self URI (journal page): https://ewic.bcs.org/

A Tool for Developing Correct Programs by Refinement

Abstract