Skip to main content
SpringerLink
Log in

Kleene under a Demonic Star

  • Conference paper
  • First Online:
Algebraic Methodology and Software Technology (AMAST 2000)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1816))

Abstract

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.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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. C. J. Aarts. Galois connections presented calculationally. Eindhoven University of Technology, Dept. of Mathematics and Computer Science, July 1992.

    Google Scholar 

  2. R. Back and J. von Wright. Refinement Calculus — A Systematic Introduction. Springer, 1998.

    Google Scholar 

  3. R. C. Backhouse et al. Fixed point calculus. Inform. Proc. Letters, 53:131–136, 1995.

    Article  MathSciNet  Google Scholar 

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

    Article  MATH  Google Scholar 

  5. R. Berghammer and H. Zierer. Relational algebraic semantics of deterministic and nondeterministic programs. Theoret. Comput. Sci., 43:123–147, 1986.

    Article  MATH  MathSciNet  Google Scholar 

  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.

    Article  MATH  Google Scholar 

  7. C. Brink, W. Kahl, and G. Schmidt (eds). Relational Methods in Computer Science. Springer, 1997.

    Google Scholar 

  8. J. H. Conway. Regular Algebra and Finite Machines. Chapman and Hall, London, 1971.

    MATH  Google Scholar 

  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.

    Article  MATH  MathSciNet  Google Scholar 

  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. D. Harel, D. Kozen, and J. Tiuryn. Dynamic Logic. Forthcoming book.

    Google Scholar 

  12. E. Hehner. Predicative programming, Parts I and II. CACM, 27:134–151, 1984.

    MATH  MathSciNet  Google Scholar 

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

    Article  Google Scholar 

  14. A. Mili, J. Desharnais, and F. Mili. Relational heuristics for the design of deterministic programs. Acta Inform., 24(3):239–276, 1987.

    Article  MATH  MathSciNet  Google Scholar 

  15. H. D. Mills. The new math of computer programming. CACM, 18(1):43–48, 1975.

    MATH  MathSciNet  Google Scholar 

  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. B. Möller. Typed Kleene algebras. Universität Augsburg, Institut für Informatik, Report, 1999

    Google Scholar 

  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. G. Schmidt and T. Ströhlein. Relations and Graphs. EATCS Monographs in Computer Science, Springer-Verlag, Berlin, 1993.

    MATH  Google Scholar 

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

Download references

Author information

Authors and Affiliations

  1. Département d’informatique, Université Laval, Québec, QC, G1K 7P4, Canada

    Jules Desharnais

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

    Bernhard Möller

  3. Mathematics Department, King Saud University, P.O.Box 22452, Riyadh, 11495, Saudi Arabia

    Fairouz Tchier

Authors
  1. Jules Desharnais
    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

  3. Fairouz Tchier
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, The University of Iowa, Iowa City, IA, 52242, USA

    Teodor Rus

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Desharnais, J., Möller, B., Tchier, F. (2000). Kleene under a Demonic Star. In: Rus, T. (eds) Algebraic Methodology and Software Technology. AMAST 2000. Lecture Notes in Computer Science, vol 1816. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45499-3_26

Download citation

  • DOI: https://doi.org/10.1007/3-540-45499-3_26

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67530-3

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation