• People
• Events
• Research

Correctness-Oriented Approaches to Software Development

Abstract: 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.

PhD Thesis - Price £8.00

LFCS report ECS-LFCS-91-147 (also published as CST-76-91)

This is a 179-page PhD thesis which is available as a 195Kb gzipped DVI file or a 634Kb DVI file or a 285Kb gzipped PostScript file or a 1Mb PostScript file.