ANSI/ISO C Specification Language

The ANSI/ISO C Specification Langage (ACSL) is a behavioral specification language for C programs. The design of ACSL is inspired of JML. It also inherits a lot from the specification language of the source code analyzer Caduceus, a previous development of one of the partners in the Frama-C project.

ACSL can express a wide range of functional properties. The paramount notion in ACSL is the function contract. ACSL 1.4
Reference While many software engineering experts advocate the "function contract mindset" when designing complex software, they generally leave the actual expression of the contract to run-time assertions, or to comments in the source code. ACSL is expressly designed for writing the kind of properties that make up a function contract.

ACSL is a formal language. This means that the specifications written in ACSL can be automatically manipulated by helper programs, in the same way that a programming language is a formal language manipulated by a compiler, and by opposition to informally written comments that can only be useful to humans.

ACSL allows to write contracts that range from the low-level (“this function expects a valid pointer to int”) to the high-level (“this function expects a nonempty linked list of ints and returns the greatest of these ints”). It is expressive enough to write complete specifications for many functions, but it can also be used for writing partial specifications. Partial specifications, of which the “expects a valid pointer to int” contract is a typical example, do not describe completely the expected behavior of the function. ACSL allows you to write
complete specifications.
But it does not force you to. Function contracts written as run-time assertions are almost always partial specifications, because a complete specification would be too annoying to write in the same language as the programming language (indeed, most often this would mean programming the function a second time).

The Jessie plug-in uses Hoare-style weakest precondition computations to formally prove ACSL properties. The process can be quite automatic, thanks to external theorem provers such as Simplify, or Alt-Ergo, or more interactive, with the use of the Coq proof-assistant. Other plug-ins, such as the value analysis plug-in may also contribute to the verification of ACSL properties. They may also report static analysis results in terms of asserted new ACSL properties inside the source code.

Documentation