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.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[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);
}
------------------------

Hope this answers your question!

- 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                    |