Summary
Proof methods adequate for a wide range of computer programs have been expounded in [1] and [2]. This paper develops a method suitable for programs containing functions, and a certain kind Of jump. The method is illustrated by the proof of a useful and efficient program for table lookup by logarithmic search.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Hoare, C. A. R.: An axiomatic basis for computer programming. Comm. ACM 12, No. 10, 576–580 (October 1969).
— Procedures and parameters; an axiomatic approach, Symposium on the Semantics of Algorithmic Languages (ed. E. Engeler). Berlin-Heidelberg-New York: Springer 1971.
Dijkstra, E. W.: Go to statement considered harmful. Letter to the editor. Comm. ACM 11, No. 3, 147–148 (March 1968).
Knuth, D. E., Floyd, R.W.: Notes on avoiding “go to” statements. Technical Report No. CS 148, Computer Science Dept., Stanford, Jan. 1970.
Landin, P. J.: A correspondence between ALGOL 60 and Church's lambda notation, parts I and II. Comm. ACM 8, Nos. 2 and 3, 89–101, Feb., 158–165, Mar. (1965).
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Clint, M., Hoare, C.A.R. Program proving: Jumps and functions. Acta Informatica 1, 214–224 (1972). https://doi.org/10.1007/BF00288686
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF00288686