Springer Nature is making Coronavirus research free. View research | View latest news | Sign up for updates

Product properties and their direct verification

  • 19 Accesses


The paper presents a family of properties of programs, called product (and power) properties, for which the verification method of Floyd and Hoare are inconvenient. A (semantically) complete alternative method is proposed' The paper presents the method in both the endogenous and exogenous versions and applies them to examples. Semantic completeness and soundness are shown. The method is particularly useful for some second-order programs, having procedures as parameters.

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


  1. 1.

    Apt, K.R.: Ten years of Hoare's logic, a survey. Part I, ACM-TOPLAS 3, 4, 431–483 (1981)

  2. 2.

    Cook, S.A.: Soundness and completeness of an axiom system for program verification. SIAM J. Comput. 7, 1, 70–90 (1978)

  3. 3.

    Ernst, G.W., Navlakha, J.K., Ogden, W.F.: Verification of programs with procedure-type parameters. Acta Informat. 18, 149–169 (1982)

  4. 4.

    Francez, N., Goffman, E., Yoeli, M.: Internal memorandum. IBM Scientific Center, Haifa 1982

  5. 5.

    Floyd, R.W.: Assigning meaning to programs. Proceedings of The Symposium on Applied Mathematics, AMS, Providence, R.I., pp. 19–32, 1967

  6. 6.

    Harel, D.: First order dynamic logic. Lecture Notes in Computer Science, Vol. 68. Berlin, Heidelberg, New York: Springer 1979

  7. 7.

    Hoare, C.A.R.: An axiomatic basis for computer programming. CACM 12, 10, 576–583 (1969)

  8. 8.

    Hoare, C.A.R.: Towards a theory of parallel programming. In: Operating Systems Techniques. Hoare, C.A.R., Perrott, R. (eds.). New York: Academic Press 1972

  9. 9.

    Manna, Z.: The Correctness of Programs. JCSS 3, 2, 119–127 (1969)

  10. 10.

    Manna, Z.: Mathematical theory of computation. New York: McGraw-Hill 1979

  11. 11.

    Pratt, V.R.: Semantic considerations on Floyd-Hoare logic. Proceedings of 17th FOCS, IEEE, Houston, TX, pp. 97–100, 1979

  12. 12.

    Schwartz, R.L.: An axiomatic definition of ALGOL 68. Ph.D. thesis, UCLA 1978

Download references

Author information

Additional information

World-trade Visiting Scientist on sabbatical leave from the Computer Science Department, Technion, Haifa 32000, Israel

Rights and permissions

Reprints and Permissions

About this article

Cite this article

Francez, N. Product properties and their direct verification. Acta Informatica 20, 329–344 (1983).

Download citation


  • Information System
  • Operating System
  • Data Structure
  • Communication Network
  • Information Theory