ANSI/ISO C Specification Language

ANSI/ISO C Specification Language
Paradigm	declarative with few imperative features.
Designed by	Commissariat à l'Énergie Atomique and INRIA
Developer	Commissariat à l'Énergie Atomique and INRIA
First appeared	2008
Stable release	2008 / December 2008
Typing discipline	static
Major implementations
	an implementation is in the Frama-C platform.
Influenced by
	JML

The ANSI/ISO C Specification Language (ACSL) is a specification language for C programs, using Hoare style pre- and postconditions and invariants, that follows the design by contract paradigm. Specifications are written as C annotation comments to the C program, which hence can be compiled with any C compiler.

The current verification tool for ACSL is Frama-C.

Overview

ACSL is a Behavioral Interface Specification Language (BISL). It aims at specifying behavioral properties of C source code. The main inspiration for this language comes from the specification language of the Caduceus tool for deductive verification of behavioral properties of C programs. The specification language of Caduceus is itself inspired from JML which aims at similar goals for Java source code.

One difference with JML, is that ACSL aims at static verification and deductive verification whereas JML aims both at runtime assertion checking and static verification using for instance the ESC/Java tool.

Syntax

Let us consider the following example for the prototype of a function named incrstar:

/*@ requires \valid(p);
  @ assigns *p;
  @ ensures *p == \old(*p) + 1;
  @*/
void incrstar (int *p);

The contract is given by the comment which starts with /*@. Its meaning is as follows:

the first line is a precondition: it states that function incrstar must be called with a pointer p that points to a safely allocated memory location.
Second line is a frame clause, stating that function incrstar does not modify any memory location but the one pointed to by p.
Finally, the ensures clause is a postcondition, which specifies that the value *p is incremented by one.

Tool support

Most of the features of ACSL are supported by Frama-C.

References

Example of ACSL usage Sufficient Preconditions for Modular Assertion Checking in VMCAI 2008 pages 188-202.
An extensive tutorial ACSL By Example was written as part of the DEVICE-SOFT project at Fraunhofer FOKUS (formerly Fraunhofer FIRST)
Report mentioning the use of ACSL in teaching [1], Петренко Ольга Леонидовна and Хорошилов Алексей Владимирович.

External links

Complete ACSL specification is available from http://frama-c.cea.fr/download.html