ANSI/ISO C Specification Language
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.
| 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 current verification tool for ACSL is Frama-C.
Overview
In 1983, the American National Standards Institute (ANSI) commissioned a committee, X3J11, to standardize the C language. The first standard for C was published by ANSI. Although this document was subsequently adopted by International Organization for Standardization (ISO) and subsequent revisions published by ISO have been adopted by ANSI, the name ANSI C continues to be used.
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
Consider the following example for the prototype of a function named incrstar:
1 /*@ requires \valid(p);
2 @ assigns *p;
3 @ ensures *p == \old(*p) + 1;
4 @*/
5 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
incrstarmust be called with a pointerpthat points to a safely allocated memory location. - Second line is a frame clause, stating that function
incrstardoes not modify any memory location but the one pointed to byp. - Finally, the
ensuresclause is a postcondition, which specifies that the value*pis 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.
- ACSL by Example, a well-documented collection of ACSL specifications of simple algorithms, is developed and maintained by the VerificationGroup at Fraunhofer FOKUS
- A tutorial about Frama-C with WP and ACSL for beginners that also provides some ideas about the theory behind the tools (available also in French).
- A report on using ACSL and Frama-C to formulate and verify low-level requirements in the context of a DO-178C compliant project
- Report mentioning the use of ACSL in teaching , Петренко Ольга Леонидовна and Хорошилов Алексей Владимирович.
- At Technikum Wien ACSL and Frama-C are taught in a course on design and verification.
External links
The complete ACSL specification is available from the download page of Frama-C.