--- layout: fc_discuss_archives title: Message 57 from Frama-C-discuss on March 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Verifying recursive functions



Hello all,

Beware! if you run this example is this in the current Lithium version, 
you have to be careful with the warning issued :

Warning: [Jessie plugin] variant for recursive function ignored

Indeed, "decreases" clauses are currently unsupported by the Jessie plugin.

A more complete answer follows.

- Claude

Jens Gerlach wrote:
> Hello Boris,
> 
> the language specification of ACSL 
> (http://frama-c.cea.fr/download/acsl_1.4.pdf) contains on page 38
> the faculty function with the follwing specification.
> 
> /*@ requires n <= 12;
>   @ decreases n;
>   @*/
> int fact(int n)
> {
>     if (n <= 1) return 1;
>     return n * fact(n-1);
> }
> 
> When I run jessie on this example, then it can verify
> that the call of "fact" inside the function body satisfies the 
> "precondition for user call".
> This is of course much less then you asked for.
> 
> Let's keep trying...
> 
> Regards Jens
> 
> 
> Am 18.03.2009 um 11:56 schrieb Hollas Boris (CR/AEY1):
> 
>> 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
> 
> 
> 
> ------------------------------------------------------------------------
> 
> _______________________________________________
> 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                    |