Yifeng Chen and J.W. Sanders
November 2000, 41 pp.
This paper introduces a calculus of weakest specification for supporting reuse of established components in deriving a design (in the sense of formal methods). The weakest specifunction generalises the notions of weakest prespecification and weakest parallel environment; but instead of calculating the weakest required component of a target specification, it calculates the weakest specification function whose value refines the target when applied to an established component. In particular it overcomes the restriction of those other calculii to taking merely one required component at a time.
A general theory of specifunctions is developed and applied to a new weakest-design calculus, which involves two required components: the par-seq specifunction places one established component in parallel with one required component and the result in sequence with another required comonent to meet a given specification. The weakest par-seq specifunction is of importance in any derivation calculus for a language combining parallel and sequential composition. A complete theory for it is presented here in the context of a refinement calculus for an abstraction of PRAM and BSP programming, and the resulting calculus is applied to the derivation of a distributed algorithm for greatest common divisor.