--- layout: default css: plugin title: ACSL ---
{% include headers.html %}
ACSL

ANSI/ISO C Specification Language

Quick description

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

WP and the older Jessie 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 Alt-Ergo, Z3 or CVC4 or more interactive, with WP's built-in interactive prover or 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.

More information

  • The ACSL manual has its own repository, together with ACSL++ (its companion language for specifying C++ programs and analyzing them with the frama-clang plug-in. Pdf versions of the manual are available on the release page.
  • A comprehensive tutorial on the WP plugin and ACSL specifications is available here.
  • Another tutorial, with specifications inspired notably from C++ containers is available here.
{% include footer.html %}