---
layout: feature
css: plugin
title: ACSL
active: 4
---

<h1>ANSI/ISO C Specification Language</h1>

<h2>Quick description</h2>
<p>The ANSI/ISO C Specification Langage (ACSL) is a behavioral
specification language for C programs. The design of ACSL is
inspired of <a class="extlink" href=
			   "http://www.eecs.ucf.edu/~leavens/JML/index.shtml">JML</a>. It also
inherits a lot from the specification language of the source code
analyzer <a class="extlink" href=
			"http://caduceus.lri.fr/">Caduceus</a>, a previous development of
one of the partners in the Frama-C project.</p>
<p>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 <em>formal</em> language.</p>

<div class="sidecode">
<pre>
/*@
  requires \valid(a+(0..n-1));<span class=inline>1</span><sidenote>ACSL provides specification primitives to cover the low-level aspects of the C programming language</sidenote><point></point>

  assigns  a[0..n-1];

  ensures<span class=inline>2</span><sidenote>As a formal language, ACSL enables a precise specification of function contracts. That makes the specification not only understandable by a human, but also manipulable by an analyzer. Furthermore, as a complete specification is not always useful, the contract can be partial, it depends on what one wants to verify.</sidenote><point></point>
  \forall integer i;
    0 <= i < n ==> a[i] == 0;
*/
void set_to_0(int* a, int n){
  int i;

  /*@
    loop invariant 0 <= i <= n;
    loop invariant
    \forall integer j;<span class=inline>3</span><sidenote>It also allows more abstract reasoning through mathematical or logic types, or through the definition of high level ideas, like "the function expects a valid linked list".</sidenote><point></point>
      0 <= j < i ==> a[j] == 0;
    loop assigns i, a[0..n-1];
    loop variant n-i;
  */
  for(i = 0; i < n; ++i)
    a[i] = 0;
}
</pre>
<div class=under id=1>ACSL provides specification primitives to cover the low-level aspects of the C programming language</div>
<div class=under id=2>As a formal language, ACSL enables a precise specification of function contracts. That makes the specification not only understandable by a human, but also manipulable by an analyzer. Furthermore, as a complete specification is not always useful, the contract can be partial, it depends on what one wants to verify.</div>
<div class=under id=3>It also allows more abstract reasoning through mathematical or logic types, or through the definition of high level ideas, like "the function expects a valid linked list".</div>

</div>

<p><a href="../fc-plugins/wp.html">WP</a> and the older
<a href="../fc-plugins/jessie.html">Jessie</a>
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 <a href="../fc-plugins/eva.html">Eva</a>
plug-in, may
also contribute to the verification of ACSL properties. They may
also report static analysis results in terms of new asserted ACSL
properties inside the source code.</p>

<h2>More information</h2>
<ul>
<li>The ACSL manual has its own
  <a href="https://github.com/acsl-language/acsl/">repository</a>,
  together with ACSL++ (its companion language for specifying C++
  programs and analyzing them with the
  <a href="../fc-plugins/frama-clang.html">frama-clang</a>
  plug-in. Pdf versions of the manual are available on the
  <a href="https://github.com/acsl-language/acsl/releases">
	release page</a>.
</li>
<li>A comprehensive tutorial on
  <a href="../fc-plugins/wp.html">the WP plugin</a> and ACSL
  specifications is available
  <a href="https://allan-blanchard.fr/frama-c-wp-tutorial.html">
	here</a>.
</li>
<li>Another tutorial, with specifications inspired notably from C++
  containers is available
  <a href="https://github.com/fraunhoferfokus/acsl-by-example">
	here</a>.
</li>
</ul>