Skip to main content
SpringerLink
Log in

Formal techniques for parallel object-oriented languages

  • Conference paper
  • First Online:
Object-Based Concurrent Computing (ECOOP 1991)

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

Included in the following conference series:

  • 144 Accesses

Abstract

This paper is intended to give an overview of the formal techniques that have been developed to deal with the parallel object-oriented language POOL and several related languages. We sketch a number of semantic descriptions, using several formalism: operational semantics, denotational semantics, and a new approach to semantics, which we call layered semantics. Then we summarize the progress that has been made in formal proof systems to verify the correctness of parallel object-oriented programs. Finally we survey the techniques that we are currently developing to describe the behaviour of objects independently of their implementation, leading to linguistic support for behavioural subtyping.

This paper was written in the context of ESPRIT Basic Research Action 3020: Integration. It is a slightly revised version of an invited paper for the Concur 91 conference, published in LNCS 527.

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.

References

  1. Pierre America and Frank de Boer. A proof system for a parallel language with dynamic process creation. ESPRIT Project 415 Document 445, Philips Research Laboratories, Eindhoven, the Netherlands, October 1988. Chapter 2 (pages 121–200) of [Boe91]. A slightly shortened version was published as [AB90].

    Google Scholar 

  2. Pierre America and Frank de Boer. A sound and complete proof system for a sequential version of POOL. ESPRIT Project 415 Document 499, Philips Research Laboratories, Eindhoven, the Netherlands, 1989. Chapter 2 (pages 15–119) of [Boe91].

    Google Scholar 

  3. Pierre America and Frank de Boer. A proof system for process creation. In IFIP TC2 Working Conference on Programming Concepts and Methods, Sea of Galilee, Israel, April 2–5, 1990, pages 303–332.

    Google Scholar 

  4. Pierre America, Jaco de Bakker, Joost N. Kok, and Jan Rutten. Operational semantics of a parallel object-oriented language. In Conference Record of the 13th Symposium on Principles of Programming Languages, St. Petersburg, Florida, January 13–15, 1986, pages 194–208.

    Google Scholar 

  5. Pierre America, Jaco de Bakker, Joost N. Kok, and Jan Rutten. Denotational semantics of a parallel object-oriented language. Information and Computation, 83(2):152–205, November 1989.

    Google Scholar 

  6. Krzysztof R. Apt, Nissim Francez, and Willem Paul de Roever. A proof system for Communicating Sequential Processes. ACM Transactions on Programming Languages and Systems, 2(3):359–385, July 1980.

    Google Scholar 

  7. J. K. Annot and P. A. M. den Haan. POOL and DOOM: The object-oriented approach. In P. C. Treleaven, editor, Parallel Computers: Object-Oriented, Functional, Logic, Wiley, 1990, pages 47–79.

    Google Scholar 

  8. Peter Apers, Bob Hertzberger, Ben Hulshof, Hans Oerlemans, and Martin Kersten. PRISMA, a platform for experiments with parallelism. In Pierre America, editor, Parallel Database Systems: Proceedings of the PRISMA Workshop, Noordwijk, The Netherlands, September 24–26, 1990, Springer Lecture Notes in Computer Science 503, pages 169–180.

    Google Scholar 

  9. Pierre America, Ben Hulshef, Eddy Odijk, Frans Sijstermans, Rob van Twist, and Rogier Wester. Parallel computers for advanced information processing. IEEE Micro, 10(6):12–15, 61–75, December 1990.

    Google Scholar 

  10. Pierre America and Frank van der Linden. A parallel object-oriented language with inheritance and subtyping. In Proceedings of OOPSLA/ECOOP '90, Ottawa, Canada, October 21–25, 1990, pages 161–168.

    Google Scholar 

  11. Pierre America. A proof theory for a sequential version of POOL. ESPRIT Project 415 Document 188, Philips Research Laboratories, Eindhoven, the Netherlands, October 1986.

    Google Scholar 

  12. Pierre America. Inheritance and subtyping in a parallel object-oriented language. In ECOOP '87: European Conference on Object-Oriented Programming, Paris, France, June 15–17, 1987, Springer Lecture Notes in Computer Science 276, pages 234–242.

    Google Scholar 

  13. Pierre America. Definition of POOL2, a parallel object-oriented language. ESPRIT Project 415 Document 364, Philips Research Laboratories, Eindhoven, the Netherlands, April 1988.

    Google Scholar 

  14. Pierre America. A behavioural approach to subtyping in object-oriented programming languages. In M. Lenzerini, D. Nardi, and M. Simi, editors, Workshop on Inheritance Hierarchies in Knowledge Representation and Programming Languages, Viareggio, Italy, February 6–8, 1989, Wiley, 1991, pages 173–190. Also appeared in Philips Journal of Research, Vol. 44, No. 2/3, July 1989, pages 365–383.

    Google Scholar 

  15. Pierre America. Issues in the design of a parallel object-oriented language. Formal Aspects of Computing, 1(4):366–411, 1989.

    Google Scholar 

  16. Krzysztof R. Apt. Ten years of Hoare logic: A survey — part I. ACM Transactions on Programming Languages and Systems, 3(4):431–483, October 1981.

    Google Scholar 

  17. Pierre America and Jan Rutten. Solving reflexive domain equations in a category of complete metric spaces. Journal of Computer and System Sciences, 39(3):343–375, December 1989.

    Google Scholar 

  18. Pierre America and Jan Rutten. A layered semantics for a parallel object-oriented language. In Foundations of Object-Oriented Languages: Proceedings of the REX School/Workshop, Noordwijkerhout, The Netherlands, May 28–June 1, 1990, Springer Lecture Notes in Computer Science 489, pages 91–123. To appear in Formal Aspects of Computing.

    Google Scholar 

  19. J. W. de Bakker, editor. Languages for Parallel Architectures: Design, Semantics, Implementation Models. John Wiley & Sons, 1989.

    Google Scholar 

  20. J. A. Bergstra and J. W. Klop. Process algebra for synchronous communication. Information and Control, 60:109–137, 1984.

    Google Scholar 

  21. J. A. Bergstra and J. W. Klop. Algebra of communicating processes with abstraction. Theoretical Computer Science, 37(1):77–121, May 1985.

    Google Scholar 

  22. Frank S. de Boer. A proof rule for process creation. In Martin Wirsing, editor, Formal Description of Programming Concepts III — Proceedings of the Third IFIP WG 2.2 Working Conference, Gl. Avernæs, Ebberup, Denmark, August 25–28, 1986, North-Holland, pages 23–50.

    Google Scholar 

  23. Frank S. de Boer. A proof system for the language POOL. In Proceedings of the 17th International Colloquium on Automata, Languages, and Programming, Warwick, England, July 16–20, 1990, Springer Lecture Notes in Computer Science 443.

    Google Scholar 

  24. Frank S. de Boer. Reasoning about Dynamically Evolving Process Structures: A Proof Theory for the Parallel Object-Oriented Language POOL. PhD thesis, Free University of Amsterdam, April 15, 1991.

    Google Scholar 

  25. J. W. de Bakker and J. I. Zucker. Processes and the denotational semantics of concurrency. Information and Control, 54:70–120, 1982.

    Google Scholar 

  26. W. Damm and G. Döhmen. The POOL-machine: A top level specification for a distributed object-oriented machine. ESPRIT Project 415 Document 1, Lehrstuhl für Informatik, RWTH Aachen, West Germany, October 3, 1986.

    Google Scholar 

  27. W. Damm, G. Döhmen, and P. den Haan. Using AADL to specify distributed computer architectures: A case study. In J. W. de Bakker, editor, Deliverable 3 of the Working Group on Semantics and Proof Techniques, Chapter 1.4, ESPRIT Project 415, October 1987.

    Google Scholar 

  28. Hans Demmers and Pieter Kleingeld. SPOOL-S: An object-oriented language with behavioural subtyping. Master's thesis, University of Utrecht, Department of Computer Science, Utrecht, the Netherlands, May 1991.

    Google Scholar 

  29. J. Dugundji. Topology. Allyn and Bacon, Boston, Massachusetts, 1966.

    Google Scholar 

  30. Joost Engelfriet, George Leih, and Grzegorz Rozenberg. Net-based description of parallel object-based systems, or POTs and POPs. In Foundations of Object-Oriented Languages: Proceedings of the REX School/Workshop, Noordwijkerhout, The Netherlands, May 28–June 1, 1990, Springer Lecture Notes in Computer Science 489, pages 229–273.

    Google Scholar 

  31. R. Engelking. General Topology, volume 6 of Sigma Series in Pure Mathematics. Heldermann, Berlin, 1989.

    Google Scholar 

  32. John V. Guttag, James J. Horning, and Andrés Modet. Report on the Larch shared language, version 2.3. Report 58, DEC Systems Research Center, Palo Alto California, April 1990.

    Google Scholar 

  33. C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–580,583, October 1969.

    Google Scholar 

  34. C. A. R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8):666–677, August 1978.

    Google Scholar 

  35. Matthew Hennessy and Gordon Plotkin. Full abstraction for a simple parallel programming language. In J. Bečvář, editor, Proceedings of the 8th Symposium on Mathematical Foundations of Computer Science, Springer Lecture Notes in Computer Science 74, 1979, pages 108–120.

    Google Scholar 

  36. Jozef Hooman and Willem-P. de Roever. The quest goes on: A survey of proof systems for partial correctness of CSP. In J. W. de Bakker, W. P. de Roever, and G. Rozenberg, editors, Current Trends in Concurrency, Springer Lecture Notes in Computer Science 224, 1987, pages 343–395.

    Google Scholar 

  37. Gordon D. Plotkin. A powerdomain construction. SIAM Journal on Computing, 5(3):452–487, September 1976.

    Google Scholar 

  38. Gordon D. Plotkin. A structural approach to operational semantics. Report DAIMI FN-19, Aarhus University, Computer Science Department, Aarhus, Denmark, September 1981.

    Google Scholar 

  39. Gordon D. Plotkin. An operational semantics for CSP. In D. Bjørner, editor, Formal Description of Programming Concepts II, North-Holland, 1983, pages 199–223.

    Google Scholar 

  40. Jan Rutten. Semantic correctness for a parallel object-oriented language. SIAM Journal on Computing, 19(3):341–383, 1990.

    Google Scholar 

  41. Michael B. Smyth. Power domains. Journal of Computer and System Sciences, 16:23–36, 1978.

    Google Scholar 

  42. Alan Snyder. Encapsulation and inheritance in object-oriented programming languages. In Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages and Applications, Portland, Oregon, September 1986, pages 38–45.

    Google Scholar 

  43. P. C. Treleaven, editor. Parallel Computers: Object-Oriented, Functional, Logic. Wiley, 1990.

    Google Scholar 

  44. Frits W. Vaandrager. Process algebra semantics for POOL. Report CS-R8629, Centre for Mathematics and Computer Science, Amsterdam, the Netherlands, August 1986.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Philips Research, P.O. Box 80.000, 5600, JA Eindhoven, The Netherlands

    Pierre America

Authors
  1. Pierre America
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

M. Tokoro O. Nierstrasz P. Wegner

Rights and permissions

Reprints and permissions

Copyright information

© 1992 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

America, P. (1992). Formal techniques for parallel object-oriented languages. In: Tokoro, M., Nierstrasz, O., Wegner, P. (eds) Object-Based Concurrent Computing. ECOOP 1991. Lecture Notes in Computer Science, vol 612. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55613-3_6

Download citation

  • DOI: https://doi.org/10.1007/3-540-55613-3_6

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-55613-8

  • Online ISBN: 978-3-540-47260-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation