Procedures and Contracts
The presence of sub-routines is as important as it is challenging from the point of view of verification. In this chapter we study a form of program logic that is adequate for reasoning about programs with procedures, and moreover it is adequate for motivating the principles that are used in practice by program verification tools and standard annotation languages, as illustrated in Chaps. 9 and 10. The material studied in the present chapter covers the interprocedural level, but at the intraprocedural level the code in the body of procedures still needs to be verified; the inference systems presented in this chapter are thus meant as extensions of systems studied previously.
The chapter starts with an overview of some of the issues involved in reasoning about procedures. Subsequent sections cover in turn inference rules and verification conditions for programs consisting of mutually recursive parameterless procedures; frame conditions; procedures with parameters; and finally return values and functions.
KeywordsInference Rule Global Variable Procedure Call Program Variable Recursive Procedure
- 2.Hoare, C.A.R.: Procedures and parameters: An axiomatic approach. In: Proceedings of Symposium on Semantics of Algorithmic Languages. Lecture Notes in Mathematics, vol. 188. Springer, Berlin (1971) Google Scholar
- 8.Nipkow, T.: Hoare logics for recursive procedures and unbounded nondeterminism. In: Bradfield, J.C. (ed.) CSL. Lecture Notes in Computer Science, vol. 2471, pp. 103–119. Springer, Berlin (2002) Google Scholar
- 9.von Oheimb, D.: Hoare logic for mutual recursion and local variables. In: Pandu Rangan, C., Raman, V., Ramanujam, R. (eds.) FSTTCS. Lecture Notes in Computer Science, vol. 1738, pp. 168–180. Springer, Berlin (1999) Google Scholar