Evolutionary Software Development in the Refinement Calculus

Abstract

This thesis considers how the refinement calculus can be used to support evolutionary development of provably correct software. Our approach is to describe a modification to a specification by composing it with a specification describing the modification, and then exploit properties of the kind of composition used, to propagate the modification through an existing derivation. We consider a representative selection of techniques for composing specifications which lend themselves well to describing modifications; in particular, we consider sequential composition with assertions and coercions, a program disjunction operator, a program override operator and two program conjunction operators. We give a large collection of laws allowing propagation of modifications described using these techniques, and give examples illustrating some of the kinds of modifications that can be described in this way and how they can be implemented using the laws presented.