Abstract
This paper attempts to provide an adequate basis for formal definitions of the meanings of programs in appropriately defined programming languages, in such a way that a rigorous standard is established for proofs about computer programs, including proofs of correctness, equivalence, and termination. The basis of our approach is the notion of an interpretation of a program: that is, an association of a proposition with each connection in the flow of control through a program, where the proposition is asserted to hold whenever that connection is taken. To prevent an interpretation from being chosen arbitrarily, a condition is imposed on each command of the program. This condition guarantees that whenever a command is reached by way of a connection whose associated proposition is then true, it will be left (if at all) by a connection whose associated proposition will be true at that time. Then by induction on the number of commands executed, one sees that if a program is entered by a connection whose associated proposition is then true, it will be left (if at all) by a connection whose associated proposition will be true at that time. By this means, we may prove certain properties of programs, particularly properties of the form: ‘If the initial values of the program variables satisfy the relation R l, the final values on completion will satisfy the relation R 2’.
This work was supported by the Advanced Research Projects Agency of the Office of the Secretary of Defense (SD-146).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
McCarthy, J.: 1963, ‘A Basis for a Mathematical Theory of Computation’, in Computer Programming and Formal Systems, North-Holland, Amsterdam, pp. 33–70.
McCarthy, J.: 1962, ‘Towards a Mathematical Science of Computation’, Proc. IFIP Congr. 62, North Holland, Amsterdam, pp. 21–28.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1993 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Floyd, R.W. (1993). Assigning Meanings to Programs. In: Colburn, T.R., Fetzer, J.H., Rankin, T.L. (eds) Program Verification. Studies in Cognitive Systems, vol 14. Springer, Dordrecht. https://doi.org/10.1007/978-94-011-1793-7_4
Download citation
DOI: https://doi.org/10.1007/978-94-011-1793-7_4
Publisher Name: Springer, Dordrecht
Print ISBN: 978-94-010-4789-0
Online ISBN: 978-94-011-1793-7
eBook Packages: Springer Book Archive