--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on March 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] fact proof



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