Kleene under a Demonic Star

  • Jules Desharnais
  • Bernhard Möller
  • Fairouz Tchier
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1816)


In relational semantics, the input-output semantics of a program is a relation on its set of states. We generalize this in considering elements of Kleene algebras as semantical values. In a nondeterministic context, the demonic semantics is calculated by considering the worst behavior of the program. In this paper, we concentrate on while loops. Calculating the semantics of a loop is difficult, but showing the correctness of any candidate abstraction is much easier. For deterministic programs, Mills has described a checking method known as the while statement verification rule. A corresponding programming theorem for nondeterministic iterative constructs is proposed, proved and applied to an example. This theorem can be considered as a generalization of the while statement verification rule to nondeterministic loops.


while loop demonic semantics relational abstraction verification Kleene algebra rule generalization 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    C. J. Aarts. Galois connections presented calculationally. Eindhoven University of Technology, Dept. of Mathematics and Computer Science, July 1992.Google Scholar
  2. 2.
    R. Back and J. von Wright. Refinement Calculus — A Systematic Introduction. Springer, 1998.Google Scholar
  3. 3.
    R. C. Backhouse et al. Fixed point calculus. Inform. Proc. Letters, 53:131–136, 1995.CrossRefMathSciNetGoogle Scholar
  4. 4.
    R. C. Backhouse and J. van der Woude. Demonic operators and monotype factors. Mathematical Structures in Comput. Sci., 3(4):417–433, 1993.zbMATHCrossRefGoogle Scholar
  5. 5.
    R. Berghammer and H. Zierer. Relational algebraic semantics of deterministic and nondeterministic programs. Theoret. Comput. Sci., 43:123–147, 1986.zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    N. Boudriga, F. Elloumi, and A. Mili, On the lattice of specifications: Applications to a specification methodology. Formal Aspects of Computing, 4:544–571, 1992.zbMATHCrossRefGoogle Scholar
  7. 7.
    C. Brink, W. Kahl, and G. Schmidt (eds). Relational Methods in Computer Science. Springer, 1997.Google Scholar
  8. 8.
    J. H. Conway. Regular Algebra and Finite Machines. Chapman and Hall, London, 1971.zbMATHGoogle Scholar
  9. 9.
    J. Desharnais, N. Belkhiter, S. B. M. Sghaier, F. Tchier, A. Jaoua, A. Mili, and N. Zaguia. Embedding a demonic semilattice in a relation algebra. Theoret. Comput. Sci., 149(2):333–360, 1995.zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    J. Desharnais and B. Möller. Characterizing functions in Kleene algebras. In J. Desharnais (ed.), Proc. 5th Seminar on Relational Methods in Computer Science (RelMiCS’5). Université Laval, Canada, pages 55–64, 2000.Google Scholar
  11. 11.
    D. Harel, D. Kozen, and J. Tiuryn. Dynamic Logic. Forthcoming book.Google Scholar
  12. 12.
    E. Hehner. Predicative programming, Parts I and II. CACM, 27:134–151, 1984.zbMATHMathSciNetGoogle Scholar
  13. 13.
    D. Kozen. Kleene algebra with tests. ACM TOPLAS 19(3):427–443, 1997.CrossRefGoogle Scholar
  14. 14.
    A. Mili, J. Desharnais, and F. Mili. Relational heuristics for the design of deterministic programs. Acta Inform., 24(3):239–276, 1987.zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    H. D. Mills. The new math of computer programming. CACM, 18(1):43–48, 1975.zbMATHMathSciNetGoogle Scholar
  16. 16.
    H. D. Mills, V. R. Basili, J. D. Gannon and R. G. Hamlet. Principles of Computer Programming. A Mathematical Approach. Allyn and Bacon, Inc., 1987.Google Scholar
  17. 17.
    B. Möller. Typed Kleene algebras. Universität Augsburg, Institut für Informatik, Report, 1999Google Scholar
  18. 18.
    T. S. Norvell. Predicative semantics of loops. In R. S. Bird and L. Meertens (eds), Algorithmic Languages and Calculi, Chapman & Hall, 1997, pages 415–437.Google Scholar
  19. 19.
    G. Schmidt and T. Ströhlein. Relations and Graphs. EATCS Monographs in Computer Science, Springer-Verlag, Berlin, 1993.zbMATHGoogle Scholar
  20. 20.
    E. Sekerinski. A calculus for predicative programming. Second International Conf. on the Mathematics of Program Construction. R. S. Bird, C. C. Morgan and J. C. P. Woodcock (eds), Oxford, June 1992, Lect. Notes in Comput. Sci., Vol. 669, Springer-Verlag, 1993.Google Scholar
  21. 21.
    F. Tchier. Sémantiques relationelles demoniaques et vérification de boucles non-déterministes. Ph.D. Thesis, Département de Mathématiques, Université Laval, Canada, 1996.Google Scholar
  22. 22.
    F. Tchier and J. Desharnais. Applying a generalization of a theorem of Mills to generalized looping structures. Colloquium Science and Engineering for Software Development, organized in the memory of Dr. Harlan D. Mills, and affiliated to the 21st International Conference on Software Engineering, Los Angeles, 18 May 1999, pages 31–38.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Jules Desharnais
    • 1
  • Bernhard Möller
    • 2
  • Fairouz Tchier
    • 3
  1. 1.Département d’informatiqueUniversité LavalQuébecCanada
  2. 2.Institut für InformatikUniversität AugsburgAugsburgGermany
  3. 3.Mathematics DepartmentKing Saud UniversityRiyadhSaudi Arabia

Personalised recommendations