PROGRAM COMPOSITION VIA UNIFICATION

Program composition and compositional proof systems have proved themse lves important for simplifying the design and the verification of prog rams. The paper presents a version of the jigsaw program composition o perator previously defined in [Fix et al. (1991, 1992)]. Here, the jig saw operator is defined as the unification of its components by their most general unifier. The jigsaw operator generalizes and unifies the traditional sequential and parallel program composition operators and the newly proposed union and superposition operators. We consider a fa mily of frameworks each consisting of a programming language, a specif ication language and a compositional syntax-directed proof system. We present syntactic rules to augment any given framework in the family w ith the jigsaw operator. The augmented framework is syntax-directed an d compositional. Moreover, it is sound and complete with respect to th e given framework.