Formally Expressing what a Program Should Do: the ACSL Language

International audienceThis chapter presents ACSL, the ANSI/ISO C Specification Language, focusingon its current implementation within the Frama-C framework. As its name suggests,ACSL is meant to express precisely and unambiguously the expected behavior ofa piece of C code. It plays a central role in Frama-C, as nearly all plug-inseventually manipulate ACSL specifications, either to generate properties thatare to be verified, or to assess that the code is conforming to these specifications.It is thus very important to have a clear view of ACSL's semantics in order tobe sure that what you check with Frama-C is really what you mean. This chapter describes thelanguage in an agnostic way, independently of the various verification plug-ins thatare implemented in the platform, which are described in more details in other chapters.It contains many examples and exercises that introduce the main features of the languageand insists on the most common pitfalls that users, even experienced ones, may encounter