Advertisement

Isomorphisms between predicate and state transformers

  • Marcello Bonsangue
  • Joost N. Kok
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 711)

Abstract

We study the relation between state transformers based on directed complete partial orders and predicate transformers. Concepts like ‘predicate’, ‘liveness’, ‘safety’ and ‘predicate transformers’ are formulated in a topological setting. We treat state transformers based on the Hoare, Smyth and Plotkin power domains and consider continuous, monotonic and unrestricted functions. We relate the transformers by isomorphisms thereby extending and completing earlier results and giving a complete picture of all the relationships.

Keywords

Arbitrary Intersection Predicate Transformer Power Domain Flat Case Scott Topology 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [Abr91]
    S. Abramsky. A domain equation for bisimulation. Information and Computation, 92:161–218, 1991.Google Scholar
  2. [AP86]
    K. R. Apt and G. Plotkin. Countable nondeterminism and random assignment. Journal of the ACM, 33(4):724–767, October 1986.Google Scholar
  3. [AS85]
    B. Alpern and F.B. Schneider. Defining liveness. Information Processing Letters, 21:181–185, 1985.Google Scholar
  4. [Bac80]
    R.-J.R. Back. Correctness Preserving Program Refinements: Proof Theory and Applications, volume 131 of Mathematical Centre Tracts. Mathematical Centre, Amsterdam, 1980.Google Scholar
  5. [Bak80]
    J. W. de Bakker. Mathematical Theory of Program Corretness. Prentice-Hall, 1980.Google Scholar
  6. [BK92]
    M. Bonsangue and J. N. Kok. Semantics, orderings and recursion in the weakest precondition calculus. Technical Report CS-R9267, Centre for Mathematics and Computer Science, Amsterdam, 1992. Extended abstract to appear in the proceedings of the Rex Workshop '92 'semantics: Foundations and Applications’ LNCS 666, 1993.Google Scholar
  7. [BK93]
    M. Bonsangue and J. N. Kok. Isomorphisms between state and predicate transformers. Technical report, Centre for Mathematics and Computer Science, Amsterdam, 1993. Available through anonymous ftp from ftp.cwi.nl.Google Scholar
  8. [Bre93]
    F. van Breugel. Relating state transformation semantics and predicate transformer semantics for parallel programs. To appear, 1993.Google Scholar
  9. [Dij76]
    E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.Google Scholar
  10. [Eng77]
    R. Engelking. General Topology. Polish Scientific Publishers, 1977.Google Scholar
  11. [HP72]
    P. Hitchcock and D. Park. Induction rules and termination proofs. In International Conference on Automata, Languages and Programming, 1972.Google Scholar
  12. [Hrb87]
    K. Hrbacek. Convex Powerdomains I. Information and computation, 74:198–225, 1987.Google Scholar
  13. [Hrb89]
    K. Hrbacek. Convex Powerdomains II. Information and computation, 81:290–317, 1989.Google Scholar
  14. [Kwi91]
    M.Z. Kwiatowska. On topological characterization of behavioural properties. In G.M. Reed, A.W. Roscoe, and R.F. Wachter, editors, Topology and Category Theory in Computer Sciences — Proc. Oxford Topology Symposioum, June 1989, pages 153–177. Oxford Science Pubblications, 1991.Google Scholar
  15. [Lam77]
    L. Lamport. Proving the correctness of a multiprocess programs. IEEE Transaction on Software Eng., SE-3:125–143, 1977.Google Scholar
  16. [MM79]
    G. Milne and R. Milner. Concurrent processes and their syntax. J. ACM, 26, 2:302–321, 1979.Google Scholar
  17. [Nel89]
    G. Nelson. A generalization of Dijkstra's calculus. ACM Transaction on Programming Languages and Systems, 11-4:517–561, 1989.Google Scholar
  18. [Plo76]
    G. D. Plotkin. A powerdomain construction. SIAM J. Comput., 5:452–487, 1976.Google Scholar
  19. [Plo79]
    G. D. Plotkin. Dijkstra's predicate transformer and Smyth's powerdomain. In Proceedings of the Winter School on Abstract Software Specification, volume 86 of Lecture Notes in Computer Science, pages 527–553. Springer-Verlag, Berlin, 1979.Google Scholar
  20. [Plo81]
    G.D. Plotkin. Post-graduate lecture notes in advanced domain theory (incorporating the “Pisa Notes”). Department of Computer Science, Univ. of Edinburgh, 1981.Google Scholar
  21. [Roe76]
    W.P. de Roever. Dijkstra's predicate transformer, non-determinism, recursion, and terminations. In Mathematical foundations of computer science, volume 45 of Lecture Notes in Computer Science, pages 472–481. Springer-Verlag, Berlin, 1976.Google Scholar
  22. [Smy78]
    M.B. Smyth. Power domains. J. Comput. Syst. Sci., 16,1:23–36, 1978.Google Scholar
  23. [Smy83]
    M.B. Smyth. Power domains and predicate transformers: A topological view. In Proceedings of ICALP '83 (Barcelona), volume 154 of Lecture Notes in Computer Science, pages 662–675. Springer-Verlag, Berlin, 1983.Google Scholar
  24. [Smy92]
    M.B. Smyth. Topology. In S. Abramsky, D.M. Gabbay, and T.S.E. Malbaum, editors, Handbook of Logic in Computer Science, volume I — Background: Mathematical Structures. Oxford University Press, 1992.Google Scholar
  25. [vW90]
    J. von Wright. A Lattice-theoretical Basis for Program Refinement. PhD thesis, Abo Akademi, 1990.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Marcello Bonsangue
    • 1
  • Joost N. Kok
    • 2
  1. 1.CWIAB AmsterdamThe Netherlands
  2. 2.Department of Computer ScienceUtrecht UniversityTB UtrechtThe Netherlands

Personalised recommendations