--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on March 2009 ---
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