Skip to main content
SpringerLink
Log in

Unifying Theories of Programming That Distinguish Nontermination and Abort

  • Conference paper
Mathematics of Program Construction (MPC 2010)

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

Included in the following conference series:

Abstract

In this paper we focus on the relationship between a number of specification models. The models are formulated in the Unifying Theories of Programming of Hoare and He, but correspond to widely used specification models. We cover issues such as partial correctness, total correctness, and general correctness.

The properties we use to distinguish the models are these:

  • whether they allow the specification of assumptions about the initial state outside of which no guarantees are given about the behaviour of the program, i.e., the program may “abort”;

  • whether a specification may allow or even require nontermination as a valid (non-aborting) outcome; and

  • whether they allow the expression of tests or enabling conditions, outside of which the program has no possible behaviour.

When considering termination, we consider both an abstract model, which only distinguishes whether a program terminates or not, as well as models that include a notion of time: either abstract time representing a notion of progress or real-time.

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. Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall, Englewood Cliffs (1998)

    Google Scholar 

  2. Jones, C.B.: Systematic Software Development using VDM. Prentice-Hall, Englewood Cliffs (1986)

    MATH  Google Scholar 

  3. Back, R.J.R.: On correct refinement of programs. Journal of Computer and System Sciences 23(1), 49–68 (1981)

    Article  MATH  MathSciNet  Google Scholar 

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

    MATH  Google Scholar 

  5. Morgan, C.C.: The specification statement. ACM Trans. on Prog. Lang. and Sys. 10(3) (July 1988)

    Google Scholar 

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

    MATH  Google Scholar 

  7. Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)

    Book  MATH  Google Scholar 

  8. Spivey, J.M.: The Z Notation: A Reference Manual. Prentice-Hall, London (1989)

    MATH  Google Scholar 

  9. Hayes, I.J. (ed.): Specification Case Studies, 2nd edn. Prentice Hall, Englewood Cliffs (1993)

    MATH  Google Scholar 

  10. Hehner, E.C.R.: Termination is timing. In: van de Snepscheut, J.L.A. (ed.) MPC 1989. LNCS, vol. 375, pp. 36–47. Springer, Heidelberg (1989)

    Google Scholar 

  11. Utting, M., Fidge, C.J.: A real-time refinement calculus that changes only time. In: He, J. (ed.) Proc. 7th BCS/FACS Refinement Workshop. Electronic Workshops in Computing. Springer, Heidelberg (1996)

    Google Scholar 

  12. Hayes, I.J., Utting, M.: Coercing real-time refinement: A transmitter. In: Duke, D.J., Evans, A.S. (eds.) BCS-FACS Northern Formal Methods Workshop (NFMW’96). Electronic Workshops in Computing. Springer, Heidelberg (1997)

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

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

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

  16. Derrick, J., Boiten, E.: Refinement in Z and Object-Z. Springer, Heidelberg (2001)

    MATH  Google Scholar 

  17. Duke, R., Rose, G., Smith, G.: Object-Z: A specification language advocated for the description of standards. Computer Standards and Interfaces 17 (1995)

    Google Scholar 

  18. Smith, G.: The Object-Z Specification Language. Kluwer Academic Publishers, Dordrecht (2000)

    MATH  Google Scholar 

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

    Article  MATH  Google Scholar 

  20. Parnas, D.L., Madey, J.: Functional documents for computer systems. Sci. Comput. Program. 25(1), 41–61 (1995)

    Article  Google Scholar 

  21. Dijkstra, E.W.: Guarded commands, nondeterminacy, and a formal derivation of programs. CACM 18, 453–458 (1975)

    MATH  MathSciNet  Google Scholar 

  22. Jacobs, D., Gries, D.: General correctness: a unification of partial and total correctness. Acta Informatica 22, 67–83 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  23. Nelson, G.: A generalisation of Dijkstra’s calculus. ACM Trans. on Prog. Lang. and Sys. 11(4) (1989)

    Google Scholar 

  24. Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Springer, Heidelberg (1990)

    MATH  Google Scholar 

  25. Dunne, S.E., Stoddart, W.J., Galloway, A.J.: Specification and refinement in general correctness. In: Evans, A., Duke, D., Clark, A. (eds.) Proceedings of the 3rd Northern Formal Methods Workshop, BCS Electronic Workshops in Computing (1998)

    Google Scholar 

  26. Dunne, S.E.: Abstract commands: a uniform notation for specifications and implementations. In: Fidge, C. (ed.) Computing: The Australasian Theory Symposium (CATS 2001). Electronic Notes in Theoretical Computer Science, vol. 42, pp. 104–123. Elsevier Science BV, Amsterdam (2001)

    Google Scholar 

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

    Google Scholar 

  28. Hehner, E.C.R.: Abstractions of time. In: Roscoe, A. (ed.) A Classical Mind, pp. 191–210. Prentice Hall, Englewood Cliffs (1994)

    Google Scholar 

  29. Hehner, E.C.R.: Retrospective and prospective for unifying theories of programming. In: Dunne, S., Stoddart, B. (eds.) UTP 2006. LNCS, vol. 4010, pp. 1–17. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  30. Abadi, M., Lamport, L.: An old-fashioned recipe for real time. ACM Trans. on Prog. Lang. and Sys. 16(5), 1543–1571 (1994)

    Article  Google Scholar 

  31. Fidge, C.J., Hayes, I.J., Watson, G.: The deadline command. IEE Proceedings—Software 146(2), 104–111 (1999)

    Google Scholar 

  32. Back, R.J., von Wright, J.: Trace refinement of action systems. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 367–384. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  33. Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison Wesley, Reading (2003)

    Google Scholar 

  34. Hayes, I.J.: Procedures and parameters in the real-time program refinement calculus. Science of Computer Programming 64(3), 286–311 (2007)

    Article  MATH  MathSciNet  Google Scholar 

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

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. The University of Queensland, Brisbane, 4072, Australia

    Ian J. Hayes

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

    Steve E. Dunne

  3. Macquarie University, Sydney, Australia

    Larissa Meinicke

Authors
  1. Ian J. Hayes
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Steve E. Dunne
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Larissa Meinicke
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Département d’informatique et de génie logiciel, Pavillon Adrien-Pouliot, Université Laval, 1065 Avenue de la Médicine, G1V 0A6, Québec, Canada

    Claude Bolduc , Jules Desharnais  & Béchir Ktari ,  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hayes, I.J., Dunne, S.E., Meinicke, L. (2010). Unifying Theories of Programming That Distinguish Nontermination and Abort. In: Bolduc, C., Desharnais, J., Ktari, B. (eds) Mathematics of Program Construction. MPC 2010. Lecture Notes in Computer Science, vol 6120. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-13321-3_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-13321-3_12

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-13320-6

  • Online ISBN: 978-3-642-13321-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation