Procedures and Contracts

  • José Bacelar Almeida
  • Maria João Frade
  • Jorge Sousa Pinto
  • Simão Melo de Sousa
Part of the Undergraduate Topics in Computer Science book series (UTICS)


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.


Inference Rule Global Variable Procedure Call Program Variable Recursive Procedure 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Back, R.-J., Preoteasa, V.: Reasoning about recursive procedures with parameters. In: MERLIN ’03: Proceedings of the 2003 ACM SIGPLAN Workshop on Mechanized Reasoning about Languages with Variable Binding, pp. 1–7. ACM, New York (2003) CrossRefGoogle Scholar
  2. 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
  3. 3.
    Homeier, P.V., Martin, D.F.: Secure mechanical verification of mutually recursive procedures. Inf. Comput.187(1), 1–19 (2003) MathSciNetMATHCrossRefGoogle Scholar
  4. 4.
    Kleymann, T.: Hoare logic and auxiliary variables. Form. Asp. Comput.11(5), 541–566 (1999) MATHCrossRefGoogle Scholar
  5. 5.
    Meyer, B.: Applying “design by contract”. Computer25(10), 40–51 (1992) CrossRefGoogle Scholar
  6. 6.
    Meyer, B.: Eiffel: The Language. Prentice Hall, Hemel Hempstead (1992) MATHGoogle Scholar
  7. 7.
    Nielson, H.R., Nielson, F.: Semantics with Applications: An Appetizer. Undergraduate Topics in Computer Science. Springer, Berlin (2007) CrossRefGoogle Scholar
  8. 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. 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

Copyright information

© Springer-Verlag London Limited 2011

Authors and Affiliations

  • José Bacelar Almeida
    • 1
  • Maria João Frade
    • 2
  • Jorge Sousa Pinto
    • 1
  • Simão Melo de Sousa
    • 2
  1. 1.Depto. InformáticaUniversidade do MinhoBragaPortugal
  2. 2.Depto. InformáticaUniversidade Beira InteriorCovilhãPortugal

Personalised recommendations