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

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

My ultimate goal is to prove total correctness, ie the complete specification and termination. But I'm also happy with either partial correctness or termination.

I don't understand the assert clause in the code below:
- "0 <= n" follows from the precondition
- "n-1 < n" is a tautology
So the assert clause should always evaluate to true, irrespective of what the program does?

- Boris


/*@ 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);