iBet uBet web content aggregator. Adding the entire web to your favor.
iBet uBet web content aggregator. Adding the entire web to your favor.



Link to original content: https://doi.org/10.1007/3-540-55719-9_113
Program composition via unification | SpringerLink
Skip to main content
Springer Nature Link
Log in

Program composition via unification

  • Conference paper
  • First Online:
Automata, Languages and Programming (ICALP 1992)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 623))

Included in the following conference series:

Abstract

Program composition and compositional proof systems have proven themselves important for simplifying the design and the verification of programs. The paper extends work presented in ICALP'91 and presents a version of the jigsaw program composition operator previously defined in [FFG90, FFG91]. 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 sequential and parallel program composition operators and the newly proposed union and superposition operators. 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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. K.R. Apt: “Ten years of Hoare's logic: a survey Part I, ACM TOPLAS 3, 1981.

    Google Scholar 

  2. R.J.R. Back: “Correctness preserving program refinements: proof theory and applications,” Mathematical Centre Tracts 131, Mathematical Centre, Amsterdam, 1980.

    Google Scholar 

  3. L. Bouge, N. Francez: “A Compositional Approach to Superimposition,” 15th ACM Symp. on Principles of Programming Languages, San Diego, CA, January 1988.

    Google Scholar 

  4. M. Chandy, J. Misra: “Parallel programs design,” Addison-Wesly, 1988.

    Google Scholar 

  5. N. Francez, I.R. Forman: “Superimposition for interacting processes,” CONCUR'90, Amsterdam, August 1990. LNCS 458, J.C.M. Baeten, J.W. Klop (Eds.), Springer-Verlag, 1990.

    Google Scholar 

  6. L. Fix, N. Francez, O. Grumberg: “Semantics-driven decompositions for the verification of distributed programs,” Proc. of the IFIP working group 2.2/2.3 working conference on Programming concepts and Methods, Sea of Galilee, Israel, April 1990, North-Holland, pp. 101–123.

    Google Scholar 

  7. L. Fix, N. Francez, O. Grumberg: “Program composition and modular verification,” Proc. 18th ICALP, Madrid, July 1991. LNCS 510, J. Leach Albert, B. Monien, M. Rodriguez Artalejo (Eds.), Springer-Verlag, 1991.

    Google Scholar 

  8. L. Fix, N. Francez, O. Grumberg: “Program composition via unification,” TR 722, Technion — Israel Institute of Technology, 1992.

    Google Scholar 

  9. E.C.R. Hehner: “Predictive programming,” part I and II, Communication ACM 27, 1984.

    Google Scholar 

  10. C.A.R. Hoare: “Communicating sequential processes,” CACM 21, 8, August 1978.

    Google Scholar 

  11. S. Katz, I. Forman, M. Evangelist: “Language constructs for distributed systems,” Proc. of the IFIP working group 2.2/2.3 working conference on Programming concepts and Methods, Sea of Galilee, Israel, April 1990, North-Holland, pp. 73–100.

    Google Scholar 

  12. R. Koymans, R. Kuiper, E. Zijlstra: “Specification specified,” in R. Kuiper Ph.D. Thesis University of Eindhoven, 1989.

    Google Scholar 

  13. E.R, Olderog: “Process theory: semantics, specification and verification,” LNCS 224 J.W. de Bakker, W.P. de Roever, G. Rozenberg (Eds.), Springer-Verlag, 1986.

    Google Scholar 

  14. A. Pnueli: “In transition from global to modular temporal reasoning about programs,” Proc. Logics and Models of Concurrent Systems, Ed. K.R. Apt, Springer-Verlag, 1985.

    Google Scholar 

  15. N. Wirth: “Program development by stepwise refinement,” Communication ACM 14, 1971.

    Google Scholar 

  16. J. Zwiers, W.P. de Roever, P. van Emde Boas: “Compositionality and concurrent networks: soundness and completeness of a proof system,” Proc. 12th ICALP, Nafplion, Greece, July 1985, Springer LNCS 194, pp. 509–519.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, Technion, 32000, Haifa, Israel

    Limor Fix, Nissim Francez & Orna Grumberg

Authors
  1. Limor Fix
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nissim Francez
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Orna Grumberg
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

W. Kuich

Rights and permissions

Reprints and permissions

Copyright information

© 1992 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fix, L., Francez, N., Grumberg, O. (1992). Program composition via unification. In: Kuich, W. (eds) Automata, Languages and Programming. ICALP 1992. Lecture Notes in Computer Science, vol 623. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55719-9_113

Download citation

  • DOI: https://doi.org/10.1007/3-540-55719-9_113

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-55719-7

  • Online ISBN: 978-3-540-47278-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation