Specification transformers: a predicate transformer approach to composition

Abstract

This paper explores theories that help in (i) proving that a system composed from components satisfies a system specification given only specifications of components and the composition operator, and (ii) deducing desirable properties of components from the system specification and properties of the composition operator. The paper studies compositional systems in general without making assumptions that components are computer programs. The results obtained from such abstract representations are general but also weaker than results that can be obtained from more restrictive assumptions such as assuming that systems are parallel compositions of concurrent programs. Explorations of general theories of composition can help identify fundamental issues common to many problem domains. The theory presented here is based on predicate transformers.

Additional Information

© Springer-Verlag Berlin/Heidelberg 2004. Received: 30 May 2002/ Revised version: 16 August 2003/ Published online: 30 October 2003.

Additional details