Advertisement

Specifying C Programs

  • 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)

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.

Keywords

Memory Location Sorting Algorithm State Label Frame Condition Verification Condition 
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.

References

  1. 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. 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. 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. 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

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