meltin.net

This paper attempts to address software specification, design and implementation reuse by bringing together work from a number of areas of program development. Refinement calculi are based on wide-spectrum languages that include abstract, logical specifications, which are transformed into executable programs. Functional and relational calculi allow programs and specifications to be manipulated using higher-order operations in powerful algebraic setting. Promotion is used in the Z specification notation to allow simple operations to be reused within a more complex framework. Specification conjunction has also been used in refinement calculi as an aid to reuse. We provide a series of examples that bring various elements of these areas together. Our examples centre on programs that can be elegantly specified by a calculation of all permutations of an input list, combined with some restriction on these permutations. This paper represents work in progress, so some of the examples are incomplete and, therefore, do not serve as convincing positive examples of the method. Also, much of the work has not been completely formalised. Our main contribution is to show that the combined approach can work in some cases and, when it does work, it is extremely profitable.

Note: This is an updated version that contains the following corrections to the originally published version:

• In equations (22), (24) and (29) a distributed intersection operator was used. This has been replaced by a distributed union operator.