Skip to main content
SpringerLink
Log in

Invariants and Well-Foundedness in Program Algebra

  • Conference paper
Theoretical Aspects of Computing – ICTAC 2010 (ICTAC 2010)

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

Included in the following conference series:

Abstract

Program algebras abstract the essential properties of programming languages in the form of algebraic laws. The proof of a refinement law may be expressed in terms of the algebraic properties of programs required for the law to hold, rather than directly in terms of the semantics of a language. This has the advantage that the law is then valid for any programming language that satisfies the required algebraic properties. By characterised the important properties of programming languages algebraically we can devise simple proofs of common refinement laws. In this paper we consider standard refinement laws for sequential programs. We give simple characterisations of program invariants and well foundedness of statements.

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. Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)

    Book  MATH  Google Scholar 

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

    MATH  Google Scholar 

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

    Article  MATH  MathSciNet  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. Conway, J.H.: Regular Algebra and Finite Machines. Chapman & Hall, Boca Raton (1971)

    MATH  Google Scholar 

  6. Dunne, S.E., Hayes, I.J., Galloway, A.J.: Reasoning about loops in total and general correctness. In: Butterfield, A. (ed.) UTP 2008. LNCS, vol. 5713, pp. 62–81. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  7. Hayes, I.J.: Reasoning about real-time programs using idle-invariant assertions. In: Dong, J.S., He, J., Purvis, M. (eds.) Proceedings 7th Asia-Pacific Software Engineering Conference (APSEC 2000), pp. 16–23. IEEE Computer Society, Los Alamitos (2000)

    Chapter  Google Scholar 

  8. Hayes, I.J.: Reasoning about real-time repetitions: Terminating and nonterminating. Science of Computer Programming 43(2-3), 161–192 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  9. Hayes, I.J.: A predicative semantics for real-time refinement. In: McIver, A., Morgan, C.C. (eds.) Programming Methodology, pp. 109–133. Springer, Heidelberg (2003)

    Google Scholar 

  10. Hayes, I.J.: Termination of real-time programs: definitely, definitely not or maybe. In: Dunne, S.E., Stoddart, W.J. (eds.) UTP 2006. LNCS, vol. 4010, pp. 141–154. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  11. Hayes, I.J., Utting, M.: A sequential real-time refinement calculus. Acta Informatica 37(6), 385–448 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  12. Hayes, I.J., Dunne, S.E., Meinicke, L.: Unifying theories of programming that distinguish nontermination and abort. In: Bolduc, C., Desharnais, J., Ktari, B. (eds.) MPC 2010. LNCS, vol. 6120, pp. 178–194. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  13. Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall, Englewood Cliffs (1998)

    Google Scholar 

  14. Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. Prentice-Hall, Englewood Cliffs (1990)

    MATH  Google Scholar 

  15. Kozen, D.: Kleene algebra with tests. ACM Transactions on Programming Languages and Systems 19, 427–443 (1999)

    Article  Google Scholar 

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

    MATH  Google Scholar 

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

    Chapter  Google Scholar 

  18. von Wright, J.: Towards a refinement algebra. Sci. of Comp. Prog. 51, 23–45 (2004)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Information Technology and Electrical Engineering, The University of Queensland, Brisbane, 4072, Australia

    Ian J. Hayes

Authors
  1. Ian J. Hayes
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of York, YO10 5DD, York, United Kingdom

    Ana Cavalcanti  & Jim Woodcock  & 

  2. Departamento de Informática e Matemática Aplicaty, Universidade Federal do Rio Grande do Norte, Lagoa Nova, 59072-970, Natal-RN, Brazil

    David Deharbe

  3. Université de Paris-Sud, LRI, 91405, Orsay cedex, France

    Marie-Claude Gaudel

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hayes, I.J. (2010). Invariants and Well-Foundedness in Program Algebra. In: Cavalcanti, A., Deharbe, D., Gaudel, MC., Woodcock, J. (eds) Theoretical Aspects of Computing – ICTAC 2010. ICTAC 2010. Lecture Notes in Computer Science, vol 6255. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14808-8_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-14808-8_1

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-14807-1

  • Online ISBN: 978-3-642-14808-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation