Anzeige
Erschienen in:
2011 | OriginalPaper | Buchkapitel
8. Procedures and Contracts
verfasst von : Dr. José Bacelar Almeida, Dr. Maria João Frade, Dr. Jorge Sousa Pinto, Dr. Simão Melo de Sousa
Erschienen in: Rigorous Software Development
Verlag: Springer London
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Abstract
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.