Abstract
Two proof methods for the verification of flowchart programs will now be introduced: the inductive assertions method and the well-founded sets method. The former method applies to proofs of partial correctness, the latter to proofs of termination. These proof methods capture the essence of the reasoning used in Example 6.8 (in the case of the inductive assertions method) and Example 6.9 (in the case of the well-founded sets method). Their improvement on the ad hoc reasoning lies in the use of predicate logic which leads to more elegant notation and in that some routine proof steps are filtered out.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Historical and Bibliographical Remarks
Floyd, R. W.: Assigning meanings to programs, Proc. Symp. on Appl. Math., 19 ( Math. Aspects of Comp. Sc.), American Math. Society, New York, 1967.
Naur, P.: Proofs of algorithms by general snapshots, BIT, 6, pp. 310–316, 1966.
Manna, Z. and Pnueli, A.: Axiomatic approach to total correctness of programs Acta Inform.3 pp. 243–264, 1974.
Bergstra, J. A., Tiuryn, J., and Tucker, J. V.: Floyd’s principle, cdrrectness theories and program equivalence, Theor. Comp. Sc., 17, pp. 113–149, 1982.
Anderson, R. B.: Proving Programs Correct, John Wiley, 1979.
Greibach, S. A.: Theory of Program Structures: Schemes, Semantics, Verification, Lect. Notes in Comp. Sc., 36, Springer-Verlag, 1975.
Katz, S. and Manna, Z.: Logical analysis of programs, Studies in Automatic Programming Logic (ed. Z. Manna and R. Waldinger), pp. 93–140, North-Holland, 1977.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1987 Springer Fachmedien Wiesbaden
About this chapter
Cite this chapter
Loeckx, J., Sieber, K. (1987). The Classical Methods of Floyd. In: The Foundations of Program Verification. Series in Computer Science. Vieweg+Teubner Verlag, Wiesbaden. https://doi.org/10.1007/978-3-322-96753-4_7
Download citation
DOI: https://doi.org/10.1007/978-3-322-96753-4_7
Publisher Name: Vieweg+Teubner Verlag, Wiesbaden
Print ISBN: 978-3-322-96754-1
Online ISBN: 978-3-322-96753-4
eBook Packages: Springer Book Archive