[Frama-c-discuss] Verifying recursive functions

Claude Marché Claude.Marche at inria.fr
Fri Mar 20 09:24:50 CET 2009


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                    |










More information about the Frama-c-discuss mailing list