Skip to main content
Springer Nature Link
Log in

The axiomatic semantics of programs based on Hoare's logic

  • Published:
Save article
View saved research
Acta Informatica Aims and scope Submit manuscript

Summary

This paper is about the Floyd-Hoare Principle which says that the semantics of a programming language can be formally specified by axioms and rules of inference for proving the correctness of programs written in the language. We study the simple language WP of while-programs and Hoare's system for partial correctness and we calculate the relational semantics of WP as this is determined by Hoare's logic. This calculation is possible by using relational semantics to build a completeness theorem for the logic. The resulting semantics AX we call the axiomatic relational semantics for WP. This AX is not the conventional semantics for WP: it need not be effectively computable or deterministic, for example. A large number of elegant properties of AX are proved and the Floyd-Hoare Principle is reconsidered.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+
from €37.37 /Month
  • Starting from 10 chapters or articles per month
  • Access and download chapters and articles from more than 300k books and 2,500 journals
  • Cancel anytime
View plans

Buy Now

Price includes VAT (Netherlands)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, books and news in related subjects, suggested using machine learning.

References

  1. Apt, K.R.: Ten years of Hoare's logic. A Survey: Part 1. ACM Trans. Progr. Lang. Syst. 3, 431–483 (1981)

    Google Scholar 

  2. Andreka, H., Nemeti, I.: Completeness of Floyd Logic. Bull. Sect. Logic Wroclaw 7, 115–121 (1978)

    Google Scholar 

  3. Andreka, H., Nemeti, I., Sain, I.: A complete logic for reasoning about programs via non-standard model theory. Theor. Comput. Sci. 17, 193–212 (1982)

    Google Scholar 

  4. Andreka, H., Nemeti, I., Sain, I.: A characterization of Floyd-provable programs. In: Mathematical Foundations of Computer Science 1981, Lecture Notes in Computer Science 118. Berlin, Heidelberg, New York: Springer, pp. 162–171, 1981

    Google Scholar 

  5. de Bakker, J.W.: Mathematical theory of program correctness. London: Prentice-Hall 1980

    Google Scholar 

  6. Bergstra, J.A., Tiuryn, J., Tucker, J.V.: Floyd's Principle, correctness theories and program equivalence. Theor. Comput. Sci. 17, 113–149 (1982)

    Google Scholar 

  7. Bergstra, J.A., Tucker, J.V.: Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs. Theor. Comput. Sci. 17, 303–315 (1982)

    Google Scholar 

  8. Bergstra, J.A., Tucker, J.V.: Algebraically specified programming systems and Hoare's logic. In: International Colloquium on Automata, Languages and Programming 1981, Lecture Notes in Computer Science 115. Berlin, Heidelberg, New York: Springer pp. 348–362, 1981

    Google Scholar 

  9. Bergstra, J.A., Tucker, J.V.: The refinement of specifications and the stability of Hoare's logic. In: Logics of Programs, Lecture Notes in Computer Science 131. Berlin, Heidelberg, New York: Springer pp. 24–36, 1981

    Google Scholar 

  10. Bergstra, J.A., Tucker, J.V.: Expressiveness and the completeness of Hoare's logic. J. Comput. Syst. Sci. 25, 276–284 (1982)

    Google Scholar 

  11. Bergstra, J.A., Tucker, J.V.: Two theorems about the completeness of Hoare's logic. Information Processing Lett. 15, 143–149 (1982)

    Google Scholar 

  12. Bergstra, J.A., Tucker, J.V.: Hoare's logic and Peano's Arithmetic. Theor. Comput. Sci. 22, 265–284 (1983)

    Google Scholar 

  13. Bergstra, J.A., Tucker, J.V.: Hoare's logic for programming languages with two data types. Theor. Comput. Sci. 28, 213–221 (1984)

    Google Scholar 

  14. Cook, S.A.: Soundness and completeness of an axiomatic system for program verification. SIAM J. Comput. 7, 70–90 (1978), Corrigendum 10, 612 (1981)

    Google Scholar 

  15. Csirmaz, L.: On the completeness of proving partial correctness. Acta Cybernet. 5, 181–190 (1981)

    Google Scholar 

  16. Csirmaz, L., Paris, J.B.: A property of 2-sorted Peano models and program verification. Preprint, Math. Inst., Hungarian Academy, Budapest, 1981

    Google Scholar 

  17. Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18, 453–457 (1975)

    Google Scholar 

  18. Dijkstra, E.W.: A discipline of programming. Engelwood Cliffs: Prentice-Hall, 1976

    Google Scholar 

  19. Floyd, R.W.: Assigning meaning to programs. In: Mathematical aspects of computer science. J.T. Schwartz (ed.). AMS, pp. 19–32, 1967

  20. Goguen, J.A., Thatcher, J.W., Wagner, E.G.: An initial algebra approach to the specification, correctness and implementation of abstract data types. In: Current trends in programming methodology IV, Data structuring. R.T. Yeh (ed.). Englewood Cliffs, New Jersey: Prentice-Hall, pp. 80–149, 1978

    Google Scholar 

  21. Greif, I., Meyer, A.R.: Specifying the semantics of while programs: a tutorial and critique of a paper by Hoare and Lauer. ACM Trans. Progr. Lang. Syst. 3, 484–507 (1981)

    Google Scholar 

  22. Hoare, C.A.R.: An axiomatic basis for computer programming, Commun. ACM 12, 576–580 (1969)

    Google Scholar 

  23. Hoare, C.A.R.: Procedures and parameters: an axiomatic approach. In: Symposium on the semantics of algorithmic languages. E. Engeler (ed.). Berlin, Heidelberg, New York: Springer pp. 102–116, 1971

    Google Scholar 

  24. Hoare, C.A.R., Lauer, P.: Consistent and complementary formal theories of the semantics of programming languages. Acta Informat. 3, 135–155 (1974)

    Google Scholar 

  25. Hoare C.A.R., Wirth, N.: An axiomatic definition of the programming language PASCAL. Acta Informat. 2, 335–355 (1973)

    Google Scholar 

  26. Kröger, F.: Infinite proof rules for loops. Acta Informat. 14, 371–389 (1980)

    Google Scholar 

  27. Lauer, P.: Consistent and complementary formal theories of the semantics of programming languages, Ph. D. Thesis Queens University, Belfast, 1972

    Google Scholar 

  28. London, R.L., Guttag, J.V., Horning, J.J., Lampson, B.W., Mitchell, J.G., Popek, G.L.: Proof rules for the programming language EUCLID. Acta Informat. 10, 1–26 (1978)

    Google Scholar 

  29. Manna, Z.: The correctness of programs. J. Comput. Syst. Sci. 3, 119–127 (1969)

    Google Scholar 

  30. Mal'cev, A.I.: Constructive algebras I. Russian Math. Surveys 16, 77–129 (1961)

    Google Scholar 

  31. McGettrick, A.: The definition of programming languages, Cambridge: University Press, 1980

    Google Scholar 

  32. Meyer, A.R., Halpern, J.Y.: Axiomatic definitions of programming languages. A theoretical assessment. J. ACM 29, 555–576 (1982)

    Google Scholar 

  33. Meyer, A.R., Halpern, J.Y.: Axiomatic definitions of programming languages II. MIT Lab. Comput. Sci. TM-179 (1980)

  34. Pagan, F.G.: Formal specification of programming languages. Englewood Cliffs: Prentice-Hall, 1981

    Google Scholar 

  35. Rabin, M.O.: Computable algebra, general theory and the theory of computable fields. Trans. AMS 95, 341–360 (1960)

    Google Scholar 

  36. Schwartz, R.: An axiomatic semantic definition of ALGOL 68. UCLA Computer Science Report 7838, 1978

  37. Tucker, J.V., Zucker, J.I.: Program correctness over abstract data types, with error state semantics, Monograph (In prep.)

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Centrum voor Wiskunde en Informatica, Kruislaan 413, NL-109855, Amsterdam, The Netherlands

    J. A. Bergstra

  2. Department of Computer Studies, University of Leeds, LS29JT, Leeds, UK

    J. V. Tucker

Authors
  1. J. A. Bergstra
    View author publications

    Search author on:PubMed Google Scholar

  2. J. V. Tucker
    View author publications

    Search author on:PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

Bergstra, J.A., Tucker, J.V. The axiomatic semantics of programs based on Hoare's logic. Acta Informatica 21, 293–320 (1984). https://doi.org/10.1007/BF00264252

Download citation

  • Received:

  • Issue date:

  • DOI: https://doi.org/10.1007/BF00264252

Keywords