Assignment and Procedure Call Proof Rules

ABSTRACT

The multiple assignment statement is defined in full generality—including assignment to subscripted variables and record fields—using the “axiomatic” approach of Hoare. Proof rules are developed for calls of procedures using global variables, var parameters, result parameters, and value parameters, using the idea of multiple assignment to provide understanding. An attempt is made to clarify some issues that have arisen concerning the use of rules of inference to aid in generating “verification conditions” in mechanical verifiers and the use of logical variables to denote initial values of program variables.

REFERENCES

• 1: Suad Alagic , Michael A. Arbib, Design of Well-Structured and Correct Programs, Springer-Verlag New York, Inc., Secaucus, NJ, 1991
• 2: BAUER, H.R., BECKER, S., ANO GRAHA~t, S.L. Algol W language description. Tech. Rep. CS89, Computer Science Dep., Stanford Univ., 1968.
• 3: Robert Cartwright , Derek Oppen, Unrestricted procedure calls in Hoare's logic, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.131-140, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512774]
• 4: CooK, S.A. Soundness and completeness of an axiomatic system for program verification. Siam J. Comput. 7 (Feb. 1978), 70-90.
• 5: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 6: James Edward Donahue, Complementary Definitions of Programming Language Semantics, Springer-Verlag New York, Inc., Secaucus, NJ, 1976
• 7: ERNST, G.W. Rules of inference for procedure calls. Acta Inf. 8 (1977), 145-152.
• 8: GRXES, D. The multiple assignment statement. IEEE Trans. Softw. Eng. SE-4 (March 78), 89- 93.
• 9: GUTTAG, J.V., HORNING, J.J., AND LONDON, R.L. A proof rule for Euclid procedures. IS/RR-77- 60, May 1977 (ARPA Order No. 2223).
• 10: HOARE, C.A.R. Procedures and parameters: An axiomatic approach. In Symp. Semantics of Algorithmic Languages, E. Engeler, Ed., Notes in Mathematics 188, Springer-Verlag, New York, 1971, pp. 102-116.
• 11: HOARE, C.A.R., AND WIRTH, N. An axiomatic definition of the programming language Pascal. Acta Inf. 2 (1973), 335-355.
• 12: IGARASHI, S., LONDON, R.L., AND LUCKHAM, D.C. Automatic program verification I: A logical basis and its implementation. Acta inf. 4 (1975), 145-182.
• 13: B. W. Lampson , J. J. Horning , R. L. London , J. G. Mitchell , G. J. Popek, Report on the programming language Euclid, ACM SIGPLAN Notices, v.12 n.2, p.1-79, February 1977 [doi>10.1145/954666.971189]
• 14: LONDON, R.L., GUTrAG, J.V., HORNIN6, J.J., LAMPSON, B.W., MITCHELL, J.G., AND POPEK, G.J. Proof rules for the programming language Euclid. Acta Inf. 10 (1978), 1-26.
• 15: David C. Luckham , Norihisa Suzuki, Verification of Array, Record, and Pointer Operations in Pascal, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.2, p.226-244, Oct. 1979 [doi>10.1145/357073.357078]
• 16: WULr, W.A., LONDON, R.L., AND SHAW, M. An introduction to the construction and verification of Alphard programs. IEEE Trans. Softw. Eng. SE-2 (Dec. 1976), 253-265.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Procedures, functions, and subroutines

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

General Terms:
Design, Languages, Performance, Theory, Verification