--- layout: fc_discuss_archives title: Message 100 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Jessie] loop invariant




On 09/12/2013 08:06 PM, Rovedy Aparecida Busquim e Silva wrote:
> Hi,
> 
> We have run the example as suggested by Claude
> (http://proval.lri.fr/gallery/ScalarProduct.en.html).
> 
> We used the example annotations in our code (attached) and the all VCs
> were proved.
> 
> However, we have some doubts:
> 
> 1. We have used the lemma bound_int_to_real but we did not understand
> how it works.
> Why the define NMAXR is used?

the lemma says the if some integer n is less or equal 3, then when
converting it to a rel number the result is less or equal 3.0. Seems
stupid but needed to help provers...

> 2. The variable j used in the loop was global in the legacy source
> code. However, the loop invariant  was not proved (loop invariant
> \abs(p - sum(x,j)) <= j * BOUND).
>   We changed the variable j to local and the loop invariant was proved.
>   Does not the loop invariant work with global variable?

It should not make any major difference. However since the context of
the VC would be a bit different (e.g. not the same order of hypotheses),
you may need to increase a little the time limit given to the prover.

I tried your example and I've been abble to prove it, both in case j is
global and when it is local. Although, I needed to modify a bit the
annotations: removing the "loop assigns p,j" that disturbs Jessie, and
replacing "sum(x,...)" by "sum(x+0,...)" because it is refused by
Frama-C kernel. I'm using Frama-C Fluorine 20130601 + Why 2.33 + Why3 +
provers Alt-Ergo, CVC3 and Gappa.

Hope this helps,

- Claude


> Best regards,
> Nanci, Luciana e Rovedy
> 
> 
> 
> 
> 2013/9/7 Claude Marche <Claude.Marche at inria.fr>
>>
>>
>>
>> On 09/07/2013 10:56 AM, Claude Marche wrote:
>>>>
>>>> Alternatively, you can force the computation into float in sum
>>>> by modifying your axiom:
>>>>    @   axiom sum2{L} :
>>>>    @     \forall float *t, integer i, j;
>>>>    @       sum(t,i,j+1) == (float)(sum(t,i,j) + t[j]);
>>>> But this is not a very good idea IMHO: as floating point addition is
>>
>>
>> A very bad idea indeed.
>>
>> - claude
>>
>>
>> _______________________________________________
>> Frama-c-discuss mailing list
>> Frama-c-discuss at lists.gforge.inria.fr
>> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>>
>>
>> _______________________________________________
>> Frama-c-discuss mailing list
>> Frama-c-discuss at lists.gforge.inria.fr
>> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss