Skip to main content
SpringerLink
Log in

Modal Design Algebra

  • Conference paper
Unifying Theories of Programming (UTP 2006)

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

Included in the following conference series:

Abstract

We give an algebraic model of the designs of UTP based on a variant of modal semirings, hence generalising the original relational model. This is intended to exhibit more clearly the algebraic principles behind UTP and to provide deeper insight into the general properties of designs, the program and specification operators, and refinement. Moreover, we set up a formal connection with general and total correctness of programs as discussed by a number of authors. Finally we show that the designs form a left semiring and even a Kleene and omega algebra. This is used to calculate closed expressions for the least and greatest fixed-point semantics of the demonic while loop that are simpler than the ones obtained from standard UTP theory and previous algebraic approaches.

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

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Backhouse, R.C., van der Woude, J.: Demonic operators and monotype factors. Mathematical Structures in Computer Science 3, 417–433 (1993)

    Article  MATH  Google Scholar 

  2. Berghammer, R., Zierer, H.: Relational algebraic semantics of deterministic and non-deterministic programs. Theoretical Computer Science 43, 123–147 (1986)

    Article  MathSciNet  MATH  Google Scholar 

  3. Broy, M., Gnatz, R., Wirsing, M.: Semantics of nondeterministic and non-continuous constructs. In: Gerhart, S.L., Pair, C., Pepper, P.A., Wössner, H., Dijkstra, E.W., Guttag, J.V., Owicki, S.S., Partsch, H., Bauer, F.L., Gries, D., Griffiths, M., Horning, J.J., Wirsing, M. (eds.) Program Construction. LNCS, vol. 69, pp. 553–592. Springer, Heidelberg (1979)

    Chapter  Google Scholar 

  4. 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 

  5. Desharnais, J., Belkhiter, N., Sghaier, S.B.M., Tchier, F., Jaoua, A., Mili, A., Zaguia, N.: Embedding a demonic semilattice in a relation algebra. Theoretical Computer Science 149, 333–360 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  6. Desharnais, J., Mili, A., Nguyen, T.T.: Refinement and demonic semantics. In: Brink, C., Kahl, W., Schmidt, G. (eds.) Relational methods in computer science, ch. 11, pp. 166–183. Springer, Heidelberg (1997)

    Google Scholar 

  7. Desharnais, J., Möller, B., Struth, G.: Kleene algebra with domain. ACM TOCL (to appear)

    Google Scholar 

  8. Desharnais, J., Möller, B., Tchier, F.: Kleene under a modal demonic star. Journal of Logic and Algebraic Programming (Special Issue on Relation Algebra and Kleene Algebra) 66(2), 127–160 (2006)

    MATH  Google Scholar 

  9. Doornbos, H.: A relational model of programs without the restriction to Egli-Milner-monotone constructs. In: Olderog, E.-R. (ed.) Programming concepts, methods and calculi, pp. 363–382. North-Holland, Amsterdam (1994)

    Google Scholar 

  10. Dunne, S.: Recasting Hoare and He’s unifying theory of programs in the context of general correctness. In: Butterfield, A., Strong, G., Pahl, C. (eds.) 5th Irish Workshop on Formal Methods. EWiC, The British Computer Society (2001)

    Google Scholar 

  11. Guttmann, W.: Non-termination in Unifying Theories of Programming. In: MacCaull, W., Winter, M., Düntsch, I. (eds.) RelMiCS 2005. LNCS, vol. 3929, pp. 108–120. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  12. Guttmann, W., Möller, B.: Modal design algebra. Institut für Informatik, Universität Augsburg, Report 2005-15

    Google Scholar 

  13. Hoare, C.A.R., He, J.: Unifying theories of programming. Prentice-Hall, Englewood Cliffs (1998)

    Google Scholar 

  14. Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Information and Computation 110, 366–390 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  15. Kozen, D.: Kleene algebra with tests. ACM TOPLAS 19, 427–443 (1997)

    Article  Google Scholar 

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

    Chapter  Google Scholar 

  17. Möller, B., Struth, G.: Modal Kleene Algebra and Partial Correctness. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 379–393. Springer, Heidelberg (2004); Revised and extended version: Möller, B., Struth, G.: Algebras of modal operators and partial correctness. Theoretical Computer Science 351, 221–239 (2006)

    Chapter  Google Scholar 

  18. Möller, B., Struth, G.: wp is wlp. In: MacCaull, W., Winter, M., Düntsch, I. (eds.) RelMiCS 2005. LNCS, vol. 3929, pp. 200–211. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  19. Nelson, G.: A generalization of Dijkstra’s calculus. ACM TOPLAS 11, 517–561 (1989)

    Article  Google Scholar 

  20. Nguyen, T.T.: A relational model of nondeterministic programs. International J. Foundations Comp. Sci. 2, 101–131 (1991)

    Article  MATH  Google Scholar 

  21. Parnas, D.: A generalized control structure and its formal definition. Commun. ACM 26, 572–581 (1983)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Abteilung Programmiermethodik und Compilerbau, Fakultät für Informatik, Universität Ulm, D-89069, Ulm, Germany

    Walter Guttmann

  2. Institut für Informatik, Universität Augsburg, D-86135, Augsburg, Germany

    Bernhard Möller

Authors
  1. Walter Guttmann
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bernhard Möller
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computing, University of Teesside, TS1 3BA, Middlesbrough, UK

    Steve Dunne

  2. University of Teesside,  

    Bill Stoddart

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Guttmann, W., Möller, B. (2006). Modal Design Algebra. In: Dunne, S., Stoddart, B. (eds) Unifying Theories of Programming. UTP 2006. Lecture Notes in Computer Science, vol 4010. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11768173_14

Download citation

  • DOI: https://doi.org/10.1007/11768173_14

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-34752-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation