Correctness-Oriented Approaches to Software Development

This thesis reports upon the experimental development of a software system. The domain of interest of this study is the use of mathematical reasoning in software development. An experiment is devised in which a modular software system is formally specified in a variety of specification styles. These initial specifications are subsequently refined to efficiently executable implementations. The refinements of the specifications are supported by differing amounts of mathematical reasoning. The issues to be investigated are the effect of increased use of mathematical analysis in software development and the influence of specifiation and refinement style on the quality of the subsequent implementation. Implementation quality is determined by: correctness with respect to the initial formal specification; clarity of the implementation; and machine efficiency. The products of the development are the analysis of specification, refinement and implementation styles and the software system itself