Specifying C Programs
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.
KeywordsMemory Location Sorting Algorithm State Label Frame Condition Verification Condition
- 1.Baudin, P., Cuoq, P., Filliâtre, J.-C., Marché, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C Specification Language. CEA LIST and INRIA (2009–2010) Google Scholar
- 2.Burghardt, J., Gerlach, J., Hartig, K., Soto, J., Weber, C.: ACSL By Example. DEVICE-SOFT project publication. Fraunhofer FIRST Institute (January 2010) Google Scholar
- 3.Hatcliff, J., Leavens, G.T., Leino, K.R.M., Müller, P., Parkinson, P.: Behavioral interface specification languages. Technical Report CS-TR-09-01, School of EECS, University of Central Florida (2009) Google Scholar
- 4.Leavens, G.T.: Tutorial on JML, the Java modeling language. In: Stirewalt, R.E.K., Egyed, A., Fischer, B. (eds.) Proceedings of ASE’07, p. 573. ACM, New York (2007) Google Scholar