Using only a simple transition relation one cannot model commands that may or may not terminate in a given state. In a more general approach commands are relations enriched with termination vectors. We reconstruct this model in modal Kleene algebra. This links the recursive definition of the do od loop with a combination of the Kleene star and a convergence operator. Moreover, the standard wp operator coincides with the wlp operator in the modal Kleene algebra of commands. Therefore our earlier general soundness and relative completeness proof for Hoare logic in modal Kleene algebra can be re-used for wp. Although the definition of the loop semantics is motivated via the standard Egli-Milner ordering, the actual construction does not depend on Egli-Milner-isotony of the constructs involved.


Relation Algebra Algebraic Semantic Hoare Logic General Soundness Idempotent Semiring 
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.
    Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)CrossRefzbMATHGoogle Scholar
  2. 2.
    Apt, K.-R., Olderog, E.-R.: Verification of Sequential and Concurrent Programs, 2nd edn. Springer, Heidelberg (1997)CrossRefzbMATHGoogle Scholar
  3. 3.
    Backhouse, R.C., van der Woude, J.: Demonic operators and monotype factors. Mathematical Structures in Computer Science 3(4), 417–433 (1993)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Berghammer, R., Zierer, H.: Relational algebraic semantics of deterministic and non-deterministic programs. Theoretical Computer Science 43, 123–147 (1986)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    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)CrossRefGoogle Scholar
  6. 6.
    Cohen, E.: Separation and reduction. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 45–59. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  7. 7.
    Conway, J.H.: Regular algebra and finite machines. Chapman and Hall, London (1971)zbMATHGoogle Scholar
  8. 8.
    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)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    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)CrossRefGoogle Scholar
  10. 10.
    Desharnais, J., Möller, B., Struth, G.: Kleene algebra with domain. ACM Transactions on Computational Logic (to appear)Google Scholar
  11. 11.
    Desharnais, J., Möller, B., Struth, G.: Termination in modal Kleene algebra. In: Lévy, J.-J., Mayr, E., Mitchell, J. (eds.) Exploring new frontiers of theoretical informatics. IFIP International Federation for Information Processing Series, vol. 155, pp. 653–666. Kluwer, Dordrecht (2004)CrossRefGoogle Scholar
  12. 12.
    Desharnais, J., Möller, B., Tchier, F.: Kleene under a modal demonic star. Journal on Logic and Algebraic Programming, Special Issue on Relation Algebra and Kleene Algebra (to appear, 2005)Google Scholar
  13. 13.
    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
  14. 14.
    Ehm, T.: The Kleene algebra of nested pointer structures: theory and applications. Universität Augsburg, Ph.D Thesis (December 2003)Google Scholar
  15. 15.
    Guttmann, W., Möller, B.: Modal design algebra. In: Dunne, S., Stoddart, B. (eds.) UTP 2006. LNCS, vol. 4010. Springer, Heidelberg (2006); Preliminary version: Institut für Informatik, Universität Augsburg, Report 2005-15 CrossRefGoogle Scholar
  16. 16.
    Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)zbMATHGoogle Scholar
  17. 17.
    Hoare, C.A.R., He, J.: Unifying theories of programming. Prentice Hall, Englewood Cliffs (1998)zbMATHGoogle Scholar
  18. 18.
    Kozen, D.: Kleene algebras with tests. ACM TOPLAS 19, 427–443 (1997)MathSciNetCrossRefGoogle Scholar
  19. 19.
    Möller, B.: Towards pointer algebra. Science of Computer Programming 21, 57–90 (1993)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Möller, B.: Lazy Kleene algebra. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 252–273. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  21. 21.
    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)CrossRefGoogle Scholar
  22. 22.
    Möller, B., Struth, G.: WP is WLP. Institut für Informatik, Universität Augsburg, Report 2004-14 (2004)Google Scholar
  23. 23.
    Nelson, G.: A generalization of Dijkstra’s calculus. ACM Transactions on Programming Languages and Systems 11, 517–561 (1989)CrossRefGoogle Scholar
  24. 24.
    Nguyen, T.T.: A relational model of nondeterministic programs. International J. Foundations Comp. Sci. 2, 101–131 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  25. 25.
    Parnas, D.: A generalized control structure and its formal definition. Commun. ACM 26, 572–581 (1983)CrossRefzbMATHGoogle Scholar
  26. 26.
    Spivey, J.M.: Understanding Z. Cambridge University Press, Cambridge (1988)zbMATHGoogle Scholar
  27. 27.
    von Wright, J.: Towards a refinement algebra. Science of Computer Programming 51, 23–45 (2004)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Bernhard Möller
    • 1
  • Georg Struth
    • 2
  1. 1.Institut für InformatikUniversität AugsburgAugsburgGermany
  2. 2.Fakultät für InformatikUniversität der Bundeswehr MünchenNeubibergGermany

Personalised recommendations