Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.


[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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


  • Subject: [Frama-c-discuss] [Jessie] loop invariant
  • From: Claude.Marche at inria.fr (Claude Marche)
  • Date: Thu, 22 Aug 2013 21:12:26 +0200
  • In-reply-to: <CAEtoXR2DsVLvtKZM9PiFNPxx-=w11eY0sr2WNQ4ymdv74P-h4A@mail.gmail.com>
  • References: <CAEtoXR21n9RPnwGE_UQ7zDjqrNPjhhRMuG5kQdzM=SjH7z+9CA@mail.gmail.com> <52162B8A.4080703@inria.fr> <CAEtoXR2DsVLvtKZM9PiFNPxx-=w11eY0sr2WNQ4ymdv74P-h4A@mail.gmail.com>


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>