--- layout: fc_discuss_archives title: Message 31 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



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.

Best regards,
Nanci, Luciana, Rovedy
----------------------------------------------------------------------------------------
#pragma JessieIntegerModel(math)
#pragma JessieTerminationPolicy(user)
#pragma JessieFloatModel(math)

float acel[3], soma;

void test()
{
  int j;

  acel[0] = 5.0;
  acel[1] = 5.0;
  acel[2] = 5.0;

  soma = 0.0;

/*@ loop invariant 0 <= j <= 3;
    loop invariant soma >= 0.0;
    loop invariant \forall integer k; 0 <= k < 3 ==> (soma <= soma +
acel[k]);
    loop assigns j, soma;
*/
       for(j=0;j<3;j++)
       {
           soma = soma + acel[j];
       }
}



2013/8/22 Claude Marche <Claude.Marche at inria.fr>

>
>
> On 08/22/2013 04:55 PM, Rovedy Aparecida Busquim e Silva wrote:
> > Hi,
> >
> > We have a function to be proved (attached).
> >
> > To include the code annotations we followed the tutorial
> > (www.acm.org/conferences/sac/sac2013/T4-Handout.pdf
> > <http://www.acm.org/conferences/sac/sac2013/T4-Handout.pdf>).
> >
> > First, we have included the "loop assigns".
> >
> > After that, we have tried to include one "loop invariant" for each
> > variable of the "loop assigns".
> >
> > The analysis of the loop has run without errors when there were not if
> > clauses in the code. After including the if clauses the analysis has
> > given four errors.
>
> I don't understand what you mean by "without the if clauses". could you
> send exactly your other version that has no error ?
>
> Apart from that, there are dubious annotations in your code, see remark
> below
>
> > We are using the plugin Jessie, Carbon version.
>
> more than 2 years old, 3 versions appeared after, you should consider
> upgrading...
>
> > /*@ loop invariant 0 <= j <= 3;
> >     loop invariant soma >= 0.0;
> >     loop invariant \forall integer k; 0 <= k < 3 ==> (soma <= soma +
> > acel[k]);
>
> this formula is equivalent to
>
> \forall integer k; 0 <= k < 3 ==> (0 <= acel[k]);
>
> is it really what you want to specify ? It doesn't even depend on the
> loop variables.
>
> - 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130822/bf46b39e/attachment-0001.html>