--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on March 2015 ---
Hello, Le 2015-03-15 20:23, Fritjof Bornebusch a ?crit : > I have a question about the proof of recursion functions, like this one: > https://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:frequently_asked_questions#how_do_i_verify_a_recursive_function > > As far as I understand this correct, the values of the inductive proof are: > a = 1 > b = n > n = \result > > But 3! is 6 and not (b*n) = 2 * 6 = 12 > > Or do I missunderstand the proof? I think you misunderstood the proof, or more exactly the is_prod predicate. Take fact(3), by its contracts it ensures is_prod(1,3,\result). By inductive definition of is_prod, we have: forall k:integer. is_prod(1,3-1,k) && 1 <= 3 ==> is_prod(1,3,\result) (with \result == 3*k). By inductive definition of is_prod, we have: forall k':integer. is_prod(1,2-1,k') && 1 <= 2 ==> is_prod(1,2,2*k') (with 2*k'==k) By inductive definition of is_prod, we have: forall k'':integer. is_prod(1,1-1,k'') && 1 <= 1 ==> is_prod(1,1,1*k'') (with 1*k''==k') By inductive definition of is_prod, we have: is_prod(1,1-1,1) because 1 > 0. Therefore we have: is_prod(1,0,1) ==> is_prod(1,1,1) (i.e. k''==1) ==> is_prod(1,1,2) (i.e. k'==1) ==> is_prod(1,3,6) (i.e. k=2, \result==3*k=3*2) Best regards, david