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.