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