Towards an integrated refinement environment for formal program development
Reeves, S. & Grundy, J. C. (1995) Towards an integrated refinement environment for formal program development. (Working paper 95/26). Hamilton, New Zealand: University of Waikato, Department of Computer Science.
Permanent Research Commons link: https://hdl.handle.net/10289/1103
One of the main hurdles to the general adoption of formal program development techniques is a lack of tools to support their use in combination with more traditional development techniques. This paper describes an integrated environment for software development which embodies the aim of formal program development. Multiple levels of refinement of each specification are supported, with associated proof obligations, each of which can be viewed at various levels of detail throughout the development process. All of these formal views are kept consistent with each other and with more traditional design and implementation views. This allows software developers to specify, design, refine, prove, implement and document their software within a single integrated environment.
University of Waikato, Department of Computer Science
- 1995 Working Papers