Exploring summation and product operators in the refinement calculus

  • Ralph-Johan Back
  • Michael Butler
Contributed Lectures
Part of the Lecture Notes in Computer Science book series (LNCS, volume 947)


Product and summation operators for predicate transformers were introduced by Naumann [23] and by Martin [18] using category theoretic considerations. In this paper, we formalise these operators in the higher order logic approach to the refinement calculus of [5], prove various algebraic properties of these operators, and look at several of their applications. We look at how the product operator provides a model of simultaneous execution of statements, while the summation operator provides a simple model of late binding. We also generalise the product operator slightly to form an operator that corresponds to conjunction of specifications. We show how the product operator may be used to model extension and modification operators for programs, and how a combination of the product and summation operators may be used to model inheritance in an object-oriented programming language.


Product Operator State Component Separation Property Sequential Composition Program Variable 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    J.R. Abrial. The B-Book. To be published by Cambridge University Press, 1995.Google Scholar
  2. 2.
    R.J.R. Back. Correctness Preserving Program Refinements: Proof Theory and Applications. Tract 131, Mathematisch Centrum, Amsterdam, 1980.Google Scholar
  3. 3.
    R.J.R. Back and R. Kurki-Suonio. Decentralisation of process nets with centralised control. In 2nd ACM SIGACT-SIGOPS Symp. on Principles of Distributed Computing, pages 131–142, 1983.Google Scholar
  4. 4.
    R.J.R. Back and K. Sere. Superposition refinement of parallel algorithms. In K.A. Parker and G.A. Rose, editors, FORTE'91. North-Holland, 1992.Google Scholar
  5. 5.
    R.J.R. Back and J. von Wright. Refinement concepts formalised in higher order logic. Formal Aspects of Computing, 5:247–272, 1990.Google Scholar
  6. 6.
    R.J.R. Back and J. von Wright. Refinement Calculus. Book in preparation, Åbo Akademi, 1994.Google Scholar
  7. 7.
    M.J. Butler. A CSP Approach To Action Systems. D.Phil. Thesis, Programming Research Group, Oxford University, 1992.Google Scholar
  8. 8.
    M.J. Butler. Refinement and Decomposition of Value-Passing Action Systems. In E. Best, editor, CONCUR'93, volume LNCS 715. Springer-Verlag, 1993.Google Scholar
  9. 9.
    E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.Google Scholar
  10. 10.
    E.W. Dijkstra. From Predicate Transformers to Predicates. Manuscript EWD821, April 1982.Google Scholar
  11. 11.
    P.H.B. Gardiner and C.C. Morgan. Data refinement of predicate transformers. Theoretical Computer Science, 87:143–162, 1991.Google Scholar
  12. 12.
    J. Gutknecht. Object-Oriented Programming with Oberon. Lecture Notes from Eastern Finland Universities International Summer School on Novel Computing, Lapeenranta University of Technology, Finland, 1994.Google Scholar
  13. 13.
    J. He, C.A.R. Hoare, and J.W. Sanders. Data refinement refined. In European Symposium on Programming, volume LNCS 213. Springer-Verlag, 1986.Google Scholar
  14. 14.
    C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.Google Scholar
  15. 15.
    P.F. Hoogendijk and R.C. Backhouse. Relational programming laws in the tree, list, bag, set hierarchy. Science of Computer Programming, 22(1–2):67–105, 1994.Google Scholar
  16. 16.
    He Jifeng and C.A.R. Hoare. Categorical Semantics of Programming Languages. In Mathematical Foundations of Programming Semantics, volume LNCS 442. Springer-Verlag, 1990.Google Scholar
  17. 17.
    C.B. Jones. Systematic Software Development using VDM — Second Edition. Prentice-Hall, 1990.Google Scholar
  18. 18.
    C.E. Martin. Preordered Categories and Predicate Transformers. D.Phil. Thesis, Programming Research Group, Oxford University, 1991.Google Scholar
  19. 19.
    C.C. Morgan. Programming from Specifications. Prentice-Hall, 1990.Google Scholar
  20. 20.
    C.C. Morgan. The cuppest capjunctive capping, and Galois. In A.W. Roscoe, editor, A Classical Mind: Essays in Honour of C.A.R. Hoare. Prentice-Hall, 1994.Google Scholar
  21. 21.
    J.M. Morris. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming, 9(3):298–306, 1987.Google Scholar
  22. 22.
    H.P. Mossenboeck. Object-Oriented Programming in Oberon-2. Springer-Verlag, 1994.Google Scholar
  23. 23.
    D.A. Naumann. Two-Categories and Program Structure: Data Types, Refinement Calculi, and Predicate Transformers. Ph.D. Thesis, University of Texas at Austin, 1992.Google Scholar
  24. 24.
    D.A. Naumann. On the Essence of Oberon. In J. Gutknecht, editor, Conference on Programming Languages and System Architectures, volume LNCS 782. Springer-Verlag, 1994.Google Scholar
  25. 25.
    D.A. Naumann. Data Refinement, Call by Value, and Higher Order Programs. Accepted for publication in Formal Aspects of Computing, 1995.Google Scholar
  26. 26.
    J.M. Spivey. The Z Notation — A Reference Manual. Prentice-Hall, 1989.Google Scholar
  27. 27.
    B.M. Utting and K. Robinson. Modular reasoning in an object-oriented refinement calculus. In Mathematics of Program Construction, 1992, volume LNCS 669. Springer-Verlag, 1993.Google Scholar
  28. 28.
    J. von Wright. The lattice of data refinement. Acta Informatica, 31(2):105–135, 1994.Google Scholar
  29. 29.
    N. Ward. Adding specification constructs to the refinement calculus. In FME'93, volume LNCS 670. Springer-Verlag, 1993.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Ralph-Johan Back
    • 1
  • Michael Butler
    • 1
  1. 1.Department of Computer ScienceÅbo AkademiFinland

Personalised recommendations