Anzeige
Erschienen in:
2011 | OriginalPaper | Buchkapitel
9. Specifying C Programs
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
In this chapter we shift the focus of our study to programs written in a realistic programming language. In particular, we focus on the ANSI/ISO C Specification Language (ACSL), which is an annotation language for C programs. ACSL has scope for frame conditions, loop invariants and variants, predicates and logic functions (either defined or specified by axioms), and a state label mechanism.
In the previous chapter we have introduced contracts and the principles of contract-based verification. ACSL adheres to these principles: each C function in a program is annotated with an ACSL specification—the function’s contract. Verification of a program consisting of a number of mutually-recursive functions is completely modular: each function is verified against its own contract, assuming that all other functions are correct. The program is correct if all functions are correct.