@@ -29,11 +29,11 @@ ACSL is a <em>formal</em> language.</p>
<divclass="sidecode">
<pre>
/*@
requires \valid(a+(0..n-1));<sidenote>ACSL provides specification primitives to cover the low-level aspects of the C programming language</sidenote><point></point>
requires \valid(a+(0..n-1));<spanclass=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<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>
ensures<spanclass=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;
*/
...
...
@@ -43,7 +43,7 @@ void set_to_0(int* a, int n){
/*@
loop invariant 0 <=i<=n;
loopinvariant
\forallintegerj;<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>
\forallintegerj;<spanclass=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;
...
...
@@ -52,6 +52,10 @@ void set_to_0(int* a, int n){
a[i] = 0;
}
</pre>
<divclass=underid=1>ACSL provides specification primitives to cover the low-level aspects of the C programming language</div>
<divclass=underid=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>
<divclass=underid=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><ahref="../fc-plugins/wp.html">WP</a> and the older