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.
Buy single article
Instant access to the full article PDF.
Price includes VAT for USA
Subscribe to journal
Immediate online access to all issues from 2019. Subscription will auto renew annually.
This is the net price. Taxes to be calculated in checkout.
Apt, K.R.: Ten years of Hoare's logic, a survey. Part I, ACM-TOPLAS 3, 4, 431–483 (1981)
Cook, S.A.: Soundness and completeness of an axiom system for program verification. SIAM J. Comput. 7, 1, 70–90 (1978)
Ernst, G.W., Navlakha, J.K., Ogden, W.F.: Verification of programs with procedure-type parameters. Acta Informat. 18, 149–169 (1982)
Francez, N., Goffman, E., Yoeli, M.: Internal memorandum. IBM Scientific Center, Haifa 1982
Floyd, R.W.: Assigning meaning to programs. Proceedings of The Symposium on Applied Mathematics, AMS, Providence, R.I., pp. 19–32, 1967
Harel, D.: First order dynamic logic. Lecture Notes in Computer Science, Vol. 68. Berlin, Heidelberg, New York: Springer 1979
Hoare, C.A.R.: An axiomatic basis for computer programming. CACM 12, 10, 576–583 (1969)
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
Manna, Z.: The Correctness of Programs. JCSS 3, 2, 119–127 (1969)
Manna, Z.: Mathematical theory of computation. New York: McGraw-Hill 1979
Pratt, V.R.: Semantic considerations on Floyd-Hoare logic. Proceedings of 17th FOCS, IEEE, Houston, TX, pp. 97–100, 1979
Schwartz, R.L.: An axiomatic definition of ALGOL 68. Ph.D. thesis, UCLA 1978
World-trade Visiting Scientist on sabbatical leave from the Computer Science Department, Technion, Haifa 32000, Israel
About this article
Cite this article
Francez, N. Product properties and their direct verification. Acta Informatica 20, 329–344 (1983). https://doi.org/10.1007/BF00264278
- Information System
- Operating System
- Data Structure
- Communication Network
- Information Theory