Adding specification constructors to the refinement calculus

This paper examines how specification construction operators may be added to the refinement calctilus. These operators are useful for the incremental construction of specifications of larger systems from component specifications. The overall aim is to provide a single coherent framework, in which one may both build specifications and refine these specifications fo program code. In particular, we add generalisations of Z schema canjunction and disjunction operators to the refinement calculus. These operators have been found effective for building Z specifications of substantial systems, and our aim is to provide similar facilities within the framework of the refinement calculus. The conjunction and disjunction operators are generalised so that they may be used to combine not just specification statements (the intuitive equivalent of the Z schema), but also arbitrary programs