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
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).
Jessie and Wp plug-ins use 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 Eva 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.