ACSL

assets/css/page.css

@@ -1234,6 +1234,12 @@ details summary:before {
 .sidecode {
   width: 50%;
   overflow: hidden;
+  margin-bottom: 20px;
+}
+@media (min-width: 1024px) {
+  .sidecode {
+    margin-bottom: 25px;
+  }
 }
 .sidecode pre {
   width: 90%;
@@ -1247,10 +1253,25 @@ sidenote {
   right: -12px;
   padding-left: 11px;
   border-left: 3px solid #e9b040;
-  font-family: 'icomoon';
-  font-size: 17px;
+  font-family: 'Muli';
+  font-size: 14px;
   text-align: justify;
 }
+@media (min-width:  768px) {
+  sidenote {
+    font-size: 15px;
+  }
+}
+@media (min-width: 1024px) {
+  sidenote {
+    font-size: 16px;
+  }
+}
+@media (min-width: 1600px) {
+  sidenote {
+    font-size: 17px;
+  }
+}
 sidenote + point {
   content:'';
   display: inline-block;

html/acsl.html

@@ -7,21 +7,6 @@ active: 4
 
 <h1>ANSI/ISO C Specification Language</h1>
 
-<h2>The C language</h2>
-
-<div class="sidecode">
-<pre>int main () {
-  int x;<sidenote>This is a variable declaration. Amazing!</sidenote><point></point>
-  x = 21;
-  int y;<sidenote>Yet another variable declaration.</sidenote><point></point>
-  y = 21;
-  int z;
-  z = x + y;
-  return z;<sidenote>And this is a function return, and a not so short sidenote. Let's see how this is diplayed on the website.</sidenote><point></point>
-}
-</pre>
-</div>
-
 <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
@@ -39,25 +24,35 @@ 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. 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>
+ACSL is a <em>formal</em> language.</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. 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>
+<div class="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>
+
+  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 understanble by a human, but also manipulable by an analyzer. Furthermore, as complete specification is not always useful, the contract can be partial, it depends on 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;<sidenote>It also allows more abstract reasoning through mathematical or logic types, or through the definition of high level ideas, like "the function expect 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>
 
 <p><a href="../fc-plugins/wp.html">WP</a> and the older
 <a href="../fc-plugins/jessie.html">Jessie</a>