Program composition via unification

Program composition and compositional proof systems have proved thermselves important for simplifying the design and the verification of programs. The paper presents a version of the jigsawprogram composition operator previously defined in [Fix et al. (1991, 1992)]. Here, the jigsaw operator is defined as the unification of its components by their most general unifier. The jigsaw operator generalizes and unifies the traditional sequentialand parallelprogram composition operators and the newly proposed unionand superpositionoperators. We consider a family of frameworks each consisting of a programming language, a specification language and a compositional syntax-directed proof system. We present syntactic rules to augment any given framework in the family with the jigsaw operator. The augmented framework is syntax-directed and compositional. Moreover, it is sound and complete with respect to the given framework.