ANSI/ISO C Specification Language

Last updated
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 appeared2008
Stable release
v1.16 / 19 November 2020
Typing discipline static
Major implementations
Frama-C
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.

Contents

The current verification tool for ACSL is Frama-C. It also implements a sister language, ANSI/ISO C++ Specification Language (ACSL++), defined for 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 is intended for static verification and deductive verification whereas JML is designed both for 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:

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

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

A valid implementation of the above function would be:

voidincrstar(int*p){(*p)++;}

Tool support

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

The TrustInSoft static analyzer is a commercial derivative of Frama-C. It verifies program behavior and (with builtin rules based on the language specification) catch instances of undefined behavior. [1]

References

  1. "ACSL Properties". TrustInSoft Documentation 1.42-dev documentation.