Skip to main content
SpringerLink
Log in
Book cover

International Conference on Mathematics of Program Construction

MPC 2006: Mathematics of Program Construction pp 397–415Cite as

Refinement Algebra with Operators for Enabledness and Termination

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4014))

Abstract

Refinement algebras are abstract algebras for reasoning about programs in a total-correctness framework. We extend a reduct of von Wright’s demonic refinement algebra with two operators for modelling enabledness and termination of programs. We show how the operators can be used for expressing relations between programs and apply the algebra to reasoning about action systems.

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Back, R.-J.: Correctness Preserving Program Refinements: Proof Theory and Applications. In: Mathematical Centre Tracts, vol. 131. Mathematical Centre, Amsterdam (1980)

    Google Scholar 

  2. Back, R.-J., Kurki-Suonio, R.: Decentralisation of process nets with centralised control. In: Proc. of 2nd Ann. ACM SIGACT-SIGOPS Symp. on Principles of Distributed Computing, PODC 1983, pp. 131–142. ACM Press, New York (1983)

    Chapter  Google Scholar 

  3. Back, R.-J.: Refining atomicity in parallel algorithms. In: Odijk, E., Rem, M., Syre, J.-C. (eds.) PARLE 1989. LNCS, vol. 366, pp. 199–216. Springer, Heidelberg (1989)

    Google Scholar 

  4. Back, R.-J., Sere, K.: Stepwise refinement of action systems. Structured Programming 12(1), 17–30 (1991)

    Google Scholar 

  5. Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, Heidelberg (1998)

    MATH  Google Scholar 

  6. Back, R.-J., von Wright, J.: Reasoning algebraically about loops. Acta Inform. 36(4), 295–334 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  7. Chen, W., Udding, J.T.: Program inversion: more than fun! Sci. of Comput. Program. 15(1), 1–13 (1990)

    Article  MATH  MathSciNet  Google Scholar 

  8. Cohen, E.: Hypotheses in Kleene algebra. Telcordia (unpublished manuscript, 1994)

    Google Scholar 

  9. Cohen, E.: Separation and reduction. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 45–59. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  10. Desharnais, J., Möller, B., Struth, G.: Kleene algebra with domain. CoRR cs.LO/0310054 (2003)

    Google Scholar 

  11. Dijkstra, E.W.: A Discipline of Programming. Prentice Hall, Englewood Cliffs (1976)

    MATH  Google Scholar 

  12. Floyd, R.W.: Assigning meanings to programs. In: Schwartz, J.T. (ed.) Mathematical Aspects of Computer Science. Proc. of Symp. on Applied Math. Amer. Math. Soc., vol. XIX, pp. 19–32 (1967)

    Google Scholar 

  13. Gries, D.: The Science of Programming. Springer, Heidelberg (1981)

    MATH  Google Scholar 

  14. Höfner, P., Möller, B., Solin, K.: Omega algebra, demonic refinement algebra and commands. Technical Report 2006-11. Inst. für Informatik, Universität Augsburg (2006)

    Google Scholar 

  15. Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Inform. and Comput. 110(2), 366–390 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  16. Kozen, D.: Kleene algebra with tests. ACM Trans. on Program. Lang. and Syst. 19(3), 427–443 (1997)

    Article  Google Scholar 

  17. Möller, B.: Lazy Kleene Algebra. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 252–273. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  18. Möller, B., Struth, G.: Greedy-like algorithms in Kleene algebra. In: Berghammer, R., Möller, B., Struth, G. (eds.) RelMiCS 2003. LNCS, vol. 3051, pp. 202–215. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  19. Morgan, C.C.: Programming from Specifications, 2nd edn. Prentice-Hall, Englewood Cliffs (1994)

    MATH  Google Scholar 

  20. Nelson, G.: A generalization of Dijkstra’s calculus. ACM Trans. on Program. Lang. and Syst. 11(4), 517–561 (1989)

    Article  Google Scholar 

  21. Sampaio, A.C.A.: An Algebraic Approach To Compiler Design. World Scientific, Singapore (1997)

    Book  MATH  Google Scholar 

  22. von Wright, J.: From kleene algebra to refinement algebra. In: Boiten, E.A., Möller, B. (eds.) MPC 2002. LNCS, vol. 2386, pp. 233–262. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  23. von Wright, J.: Towards a refinement algebra. Sci. of Comput. Program. 51(1-2), 23–45 (2004)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Turku Centre for Computer Science, Lemminkäinengatan 14 A, FIN-20520, Åbo, Finland

    Kim Solin & Joakim von Wright

Authors
  1. Kim Solin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Joakim von Wright
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute of Cybernetics at Tallinn University of Technology, Akadeemia tee 21, EE-12618, Tallinn, Estonia

    Tarmo Uustalu

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Solin, K., von Wright, J. (2006). Refinement Algebra with Operators for Enabledness and Termination. In: Uustalu, T. (eds) Mathematics of Program Construction. MPC 2006. Lecture Notes in Computer Science, vol 4014. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11783596_23

Download citation

  • DOI: https://doi.org/10.1007/11783596_23

  • Publisher Name: Springer, Berlin, Heidelberg

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation