Commit a1517aca authored by MARCHE Claude's avatar MARCHE Claude

polished doc

parent 80c78d75
digraph G {
graph [nodesep=0.5,
rankdir=TB,
ranksep=0.5
];
node [margin=0.05,shape=ellipse];
"entry" -> "L" [label=" i <- 0" ];
graph [bgcolor=lightgray; rankdir="TB"];
node [margin=0.05,shape=ellipse,style=filled,fillcolor="cyan"];
"entry" [pos="2,3!"];
"L" [pos="2,2!"];
"invariant" [pos="2,1!"];
"cond" [pos="2,0!"];
"do" [pos="0,1!"];
"exit" [pos="4,0!"];
"entry" -> "L" [label=" i <- 0"];
"L" -> "invariant" [label=" m <- a[i]"];
"invariant" -> "cond" [label=" i <- i+1"];
"cond" -> "exit" [label=" i >= n"];
"cond" -> "do" [label=" i < n"];
"do" -> "L" [label=" a[i] > m"];
"do" -> "L" [label=" a[i] > m"; headport=e];
"do" -> "invariant" [label=" a[i] <= m"];
"cond" -> "exit" [label=" i >= n"];
}
......@@ -382,26 +382,26 @@ An example
~~~~~~~~~~
The following example comes from the documentation of the ANSI C Specification Language
\cite{baudinXXacsl, section 2.4.2 Loop invariants).
(See :cite:`baudin18acsl`, section 2.4.2 Loop invariants, Example 2.27).
::
.. code-block:: C
/*@ requires n >= 0 && \valid(a,0,n);
@ ensures \forall integer j ; 0 <= j < n ==> \result >= a[j])
@ ensures \forall integer j ; 0 <= j < n ==> \result >= a[j]);
@*/
int max_array(int a[], int n) {
int m, i = 0;
goto L;
do {
if (a[i] > m) { L: m = a[i]; }
/*@ invariant
@ 0 <= i < n && \forall integer j ; 0 <= j <= i ==> m >= a[j]);
@*/
i++;
}
while (i < n);
return m;
}
if (a[i] > m) { L: m = a[i]; }
/*@ invariant
@ 0 <= i < n && \forall integer j ; 0 <= j <= i ==> m >= a[j]);
@*/
i++;
}
while (i < n);
return m;
}
The code can be viewed as a control-flow graph as shown in :numref:`fig.cfg.max_array`.
......@@ -409,8 +409,8 @@ The code can be viewed as a control-flow graph as shown in :numref:`fig.cfg.max_
:caption: Control-Flow Graph of "max_array" example
:name: fig.cfg.max_array
Here is a version in the Why3-CFG language, where label L corresponds
to node L, label L1 to node 'invariant', label L2 to node "do".
Here is below a version of this code in the Why3-CFG language, where label "L" corresponds
to node "L", label "L1" to node "invariant", label "L2" to node "do".
::
......@@ -448,11 +448,12 @@ to node L, label L1 to node 'invariant', label L2 to node "do".
end
}
The consecutive invariants act as one cut in the generation of VCs.
Limitations
~~~~~~~~~~~
Current Limitations
~~~~~~~~~~~~~~~~~~~
- Termination is never checked
......@@ -460,3 +461,6 @@ Limitations
- Trailing code after "switch" is not supported: switch branches must
return a value or end with a goto
- Conditional statements "if e then i1 else i2" are not yet supported, but can be
simulated with "switch (e) | True -> i1 | False -> i2 end"
......@@ -180,3 +180,13 @@
year = 2018,
keywords = {Deductive Program Verification ; Weakest Precondition Calculus ; Satisfiability Modulo Theories ; Counterexamples}
}
@Manual{baudin18acsl,
title = {{ACSL}: {ANSI/ISO C} Specification Language},
author = {Patrick Baudin and Jean-Christophe Filliâtre and Claude Marché and Benjamin Monate and Yannick Moy and Virgile Prevosto},
year = 2018,
note = {\url{https://frama-c.com/acsl.html}},
url = {https://frama-c.com/acsl.html},
x-pdf = {https://frama-c.com/download/acsl_1.14.pdf}
}
Markdown is supported
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