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

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




On 08/22/2013 07:02 PM, Rovedy Aparecida Busquim e Silva wrote:
> Hi,
> 
> We are sending the working version of the code without the if statements.
> 
> According to tutorial, we have followed the below sequence:
> - identify variables modified in the loop:
> - use loop assigns clause to list variables that (might) have been
> assigned so far after iterations
> - define their possible value intervals (relationships) after iterations
>  
> In our case, we identified the variables j and soma that were modified
> in the loop.
> 
> Because of that, we tried to specify the variable soma.

I think the question you should ask yourself is what would you like to
specify about soma first, in English.

It is seems natural to specify that at each loop iteration, soma is the
sum of elements of array acel for index between 0 to j-1.

I recommend to look at the example tests/c/sum_array.c of the Why 2.33
distrib. Here it is as attachment


> float acel[3], soma;
>  
> void test()
> {
>   int j;
>   
>   acel[0] = 5.0;  
>   acel[1] = 5.0;
>   acel[2] = 5.0;
>   
>   soma = 0.0;


There is a big difference in this version: values acel[0..] are
initialized. It is then clear true that all acel[k], for 0<=k<3, are
>= 0

The formula in the loop inv is thus true,


-------------- section suivante --------------
Une pi?ce jointe autre que texte a ?t? nettoy?e...
Nom: sum_array.c
Type: text/x-csrc
Taille: 1492 octets
Desc: non disponible
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130822/edaf65dc/attachment.c>