Skip to content
Snippets Groups Projects
Commit 39c3dd28 authored by Augustin Lemesle's avatar Augustin Lemesle
Browse files

Merge branch 'acsl' into 'master' 

New page about the ACSL language.

See merge request !20
parents f767b18c 71838fe0
No related branches found
No related tags found
1 merge request!20New page about the ACSL language.
Pipeline #24112 passed
Stage: deploy
    Hide whitespace changes
    Inline Side-by-side
    _layouts/plugin.html
    + 1
    − 1
    View file @ 39c3dd28
    ...@@ -13,7 +13,7 @@ css: plugin ...@@ -13,7 +13,7 @@ css: plugin
    <div> <div>
    <a href="/html/kernel-plugin.html"><i class="icon-arrow-left"></i>Back</a> <a href="/html/kernel-plugin.html"><i class="icon-arrow-left"></i>Back</a>
    </div><a class="tabLink active" href="/html/kernel-plugin.html">Plugins</a> <em></em> <a class="tabLink" href= </div><a class="tabLink active" href="/html/kernel-plugin.html">Plugins</a> <em></em> <a class="tabLink" href=
    "/html/kernel.html">Kernel</a> <em></em> <a class="tabLink" href="/html/gui.html">GUI</a> "/html/kernel.html">Kernel</a> <em></em> <a class="tabLink" href="/html/acsl.html">ACSL</a>
    </div> </div>
    </div> </div>
    ......
    html/acsl.html 0 → 100755
    + 83
    − 0
    View file @ 39c3dd28
    ---
    layout: default
    css: plugin
    title: ACSL
    ---
    <body class="page-template page-template-page-kernel page-template-page-kernel-php page page-id-179 nonTouch">
    <div id="wrapper" class="hfeed">
    {% include headers.html %}
    <div id="container" class="mainContainer">
    <div class="tabs">
    <div class="wrap">
    <a class="tabLink" href="/html/kernel-plugin.html">Plugins</a> <em></em> <a class="tabLink" href=
    "/html/kernel.html">Kernel</a> <em></em> <a class="tabLink active" href="/html/acsl.html">ACSL</a>
    </div>
    </div>
    <div class="pageKernel pages">
    <div class="bgTextbig">
    ACSL
    </div>
    <div class="wrap">
    <h1>ANSI/ISO C Specification Language</h1>
    <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. <span class=
    "slogan"><a class="pdf" href="download/acsl.pdf">ACSL<br />
    Reference</a></span> 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.</p>
    <p>ACSL is a <em>formal</em> 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.</p>
    <p>ACSL allows to write contracts that range from the low-level
    (“<i>this function expects a valid pointer to int</i>”) to the
    high-level (“<i>this function expects a nonempty linked list of
    ints and returns the greatest of these ints</i>”). 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 “<i>expects a valid pointer to
    int</i>” contract is a typical example, do not describe completely
    the expected behavior of the function. <span class="slogan">ACSL
    allows you to write<br />
    complete specifications.<br />
    But it does not force you to.</span> 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).</p>
    <p><a href="jessie.html">Jessie</a> and <a href="wp.html">Wp</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 Simplify, or Alt-Ergo,
    or more interactive, with the use of the Coq proof-assistant. Other
    plug-ins, such as the <a href="value.html">Eva</a> 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.</p>
    </div>
    </div>
    {% include footer.html %}
    <div class="clear"></div>
    </div>
    </div>
    </body>
    html/gui.html deleted 100755 → 0
    + 0
    − 37
    View file @ f767b18c
    ---
    layout: default
    css: plugin
    title: GUI - Frama-C
    ---
    <body class="page-template page-template-page-kernel page-template-page-kernel-php page page-id-179 nonTouch">
    <div id="wrapper" class="hfeed">
    {% include headers.html %}
    <div id="container" class="mainContainer">
    <div class="tabs">
    <div class="wrap">
    <a class="tabLink" href="/html/kernel-plugin.html">Plugins</a> <em></em> <a class="tabLink" href=
    "/html/kernel.html">Kernel</a> <em></em> <a class="tabLink active" href="/html/gui.html">GUI</a>
    </div>
    </div>
    <div class="pageKernel pages">
    <div class="bgTextbig">
    GUI
    </div>
    <div class="wrap">
    <p> Write something </p>
    </div>
    </div>
    {% include footer.html %}
    <div class="clear"></div>
    </div>
    </div>
    </body>
    html/kernel-plugin.html
    + 1
    − 1
    View file @ 39c3dd28
    ...@@ -13,7 +13,7 @@ title: Kernel & Plugins - Frama-C ...@@ -13,7 +13,7 @@ title: Kernel & Plugins - Frama-C
    <div class="tabs"> <div class="tabs">
    <div class="wrap"> <div class="wrap">
    <a class="active tabLink" href="kernel-plugin.html">Plugins</a> <em></em> <a class="tabLink" href= <a class="active tabLink" href="kernel-plugin.html">Plugins</a> <em></em> <a class="tabLink" href=
    "/html/kernel.html">Kernel</a> <em></em> <a class="tabLink" href="/html/gui.html">GUI</a> "/html/kernel.html">Kernel</a> <em></em> <a class="tabLink" href="/html/acsl.html">ACSL</a>
    <div class="tabOptions"> <div class="tabOptions">
    <div class="pluginSearch"> <div class="pluginSearch">
    ......
    html/kernel.html
    + 1
    − 1
    View file @ 39c3dd28
    ...@@ -14,7 +14,7 @@ title: Kernel & Plugins - Frama-C ...@@ -14,7 +14,7 @@ title: Kernel & Plugins - Frama-C
    <div class="tabs"> <div class="tabs">
    <div class="wrap"> <div class="wrap">
    <a class="tabLink" href="/html/kernel-plugin.html">Plugins</a> <em></em> <a class="tabLink active" href= <a class="tabLink" href="/html/kernel-plugin.html">Plugins</a> <em></em> <a class="tabLink active" href=
    "/html/kernel.html">Kernel</a> <em></em> <a class="tabLink" href="/html/gui.html">GUI</a> "/html/kernel.html">Kernel</a> <em></em> <a class="tabLink" href="/html/acsl.html">ACSL</a>
    </div> </div>
    </div> </div>
    ......
    0% or .
    You are about to add 0 people to the discussion. Proceed with caution.
    Finish editing this message first!
    Please register or to comment