--- layout: fc_discuss_archives title: Message 37 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,

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090318/3f761322/attachment.htm