Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Frama-c-discuss] Verifying recursive functions

```Your question is a bit imprecise: by "a way to verify recursive
functions", do you mean: verify there termination ? or verify some
functional behavior of them ?

Here is a way to do both in Frama-C Lithium with the Jessie plugin. This
example emphasized a few current limitations that you should be aware.
These are planned to be supported in the future.
1) decreases clauses not yet supported
2) \prod construct not yet supported
moreover, you should be aware that this code might produce arithmetic
overflow for large values of n, and this is checkd by default.

So here is an annotated code that is 100% proved, automatically (at
least with Alt-Ergo and Simplify):

--------------
// the following pragma allows to ignore potential arithmetic overflow
#pragma JessieIntegerModel(exact)

/* the \prod ACSL construct is not yet supported by the Jessie plugin
* the following inductive definition is a work-around
*/

// is_prod(a,b,n) true whenever n = prod_{i=a..b} i
/*@ inductive is_prod(integer a, integer b, integer n) {
@   case is_prod_empty :
@      \forall integer a,b; a > b ==> is_prod(a,b,1);
@   case is_prod_left :
@      \forall integer a,b,n; a <= b && is_prod(a,b-1,n)
@           ==> is_prod(a,b,b*n);
@ }
@*/

/*@ requires n >= 0;
@ ensures is_prod(1,n,\result);
@ decreases n; // not yet supported by Jessie plugin
@*/
int fact(int n) {
if (n == 0) return 1;
// simulating the VC for the decreases clause
//@ assert 0 <= n && n-1 < n;
return n * fact(n-1);
}
------------------------

- Claude

Hollas Boris (CR/AEY1) wrote:
> Hello,
>
> I use Spec# with Boogie and the Z3 SMT-solver as back-end. Yet, I haven't found a way to verify recursive functions. Therefore, I wonder whether this is possible with frama-c and the Jessie plugin.
>
> For example, consider the following recursive implementation of the factorial function:
>
>     static int fac(int n)
>     requires n >= 0;
>     ensures result == product {int i in (1..n); i};
>     {
>         if(n==0) return 1;
>         else return n*fak(n-1);
>     }
>
> Spec# is not able to prove the postcondition using default settings. Furthermore, I don't know if I can instruct Spec# or the provers to induce on n.
>
> Would frama-c be able to verify the function above?
>
> Cheers,
> Boris
>
>
>
>
> ------------------------------------------------------------------------
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

--
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |

```