Summary
A proof rule for the procedure call is derived for procedures with value, result and value-result parameters. It is extended to procedures with unrestricted global variables and to recursive procedures. Like D. Gries's proof rule, it is based on the substitution rule for assignment. However, it is more general and much simpler to apply. Assume that {U} S {V} has been proved about the procedure body S. The proof rule for determining whether a call establishes predicate E is based on finding an “adaptation” A satisfying A∧V ⇒ E′, where E′ is derived from E by some substitution of parameters.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Dijkstra, E.W.: A Discipline of Programming, Prentice Hall, Englewood Cliffs, New Jersey, 1976
Dijkstra, E.W.: Lecture Notes: Predicate transformers, EWD835, Nov. 1982
Dijkstra, E.W.: On Mathematical Induction, EWD803-22, Nov. 1981
Dijkstra, E.W., Scholten, C.S.: About Predicate Transformers in General, EWD813, March 1982
Gries, D., Levin, G.: Assignment and Procedure Call Proof Rules, TOPLAS 2, 564–579 (1980)
Gries, D.: The Science of Programming. Berlin-Heidelberg-New York: Springer-Verlag 1981
Gries, D.: Private communication, Feb. 1983
Hoare, C.A.R.: Procedures and Parameters: An Axiomatic Approach. In: Symposium on Semantics of Programming Languages, pp. 102–116. Berlin-Heidelberg-New York: Springer 1971
London, R.L., Guttag, J.V., Horning, J.J., Lampson, B.W., Mitchell, J.G., Popek, G.J.: Proof Rules for the Programming Language Euclid. Acta Informat. 10, 1–26 (1978)
Scholten, C.S.: Private communication, Feb. 1983
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Martin, A.J. A general proof rule for procedures in predicate transformer semantics. Acta Informatica 20, 301–313 (1983). https://doi.org/10.1007/BF00264276
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF00264276