Frama-C-discuss mailing list archives

rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva) · Thu, 5 Sep 2013 10:27:16 -0300

Hi,

We would like to prove that soma is the sum of elements of array.  We have
looked the example recommended (tests/c/sum_array.c -Why 2.33).

We modified the example, the int t[] was replaced to float t[] (in the
function and in the axiomatic).
When we used the Pragma it worked successful. We have observed that the
example with Pragma (sum_array_Pragma.c) proved the loop invariant. The
screen shot (Pragma.png) shows that it works with Real variable.

However, we would like to work without the pragma (with floating point
arithmetic).
The problem is that the loop invariant below was not proved:
loop invariant s == sum(t,0,i);

The screen shot (Without_Pragma.png) shows the comparison between a Real
variable and float. We think that the loop invariant was not proved because
of that.

Is this the problem? How can we to solve this problem?

The files are attached.

Best regards,
Luciana, Nanci and Rovedy

------------------------------------------------------------------------------------------------------------------------------------------------
#pragma JessieFloatModel(math)

/*@ axiomatic Sum {
  @   // sum(t,i,j) denotes t[i]+...+t[j-1]
  @   logic real sum{L}(float *t, integer i, integer j)
  @        reads i,j,t, t[..] ;
  @   axiom sum1{L} :
  @     \forall float *t, integer i; sum(t,i,i) == 0;
  @   axiom sum2{L} :
  @     \forall float *t, integer i, j;
  @       sum(t,i,j+1) == sum(t,i,j) + t[j];
  @ }
  @*/

/*@ requires n >= 1 && \valid_range(t,0,n-1) ;
  @ ensures \result == sum(t,0,n);
  @*/
float test1(float t[],int n) {
  int i;
  float s = 0.0;

  /*@ loop invariant 0 <= i <= n && s == sum(t,0,i);
    @ loop variant n-i;
  */
  for(i=0; i < n; i++)
  {
    s += t[i];
  }
  return s;
}
--------------------------------------------------------------------------------------------------------------------------------------------------
/*@ axiomatic Sum {
  @   // sum(t,i,j) denotes t[i]+...+t[j-1]
  @   logic real sum{L}(float *t, integer i, integer j)
  @        reads i,j,t, t[..] ;
  @   axiom sum1{L} :
  @     \forall float *t, integer i; sum(t,i,i) == 0;
  @   axiom sum2{L} :
  @     \forall float *t, integer i, j;
  @       sum(t,i,j+1) == sum(t,i,j) + t[j];
  @ }
  @*/

/*@ requires n >= 1 && \valid_range(t,0,n-1) ;
  requires \forall int i; 0 <= i < n ==> t[i] >= 0.0 && t[i] < 1000.0;
  @ ensures \result == sum(t,0,n);
  @*/

float test1(float t[], int n) {
  int i;
  float s = 0.0;

 /*@ loop invariant 0 <= i <= n && s == sum(t,0,i);
     loop invariant 0.0 <=  sum(t,0,i) <= i * 1000.0;
     loop assigns s;
     loop variant n-i;
  */

  for(i=0; i < n; i++)
  {
    s += t[i];
  }
  return s;
}

----------------------------------------------------------------------------------------------------------------------------

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

>
>
> 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,
>
>
>
> _______________________________________________
> 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
>

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

>
>
> 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,
>
>
>
> _______________________________________________
> 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
>

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

>
>
> 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,
>
>
>
> _______________________________________________
> 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/20130905/47d769f1/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: sum_arrayPragma.c
Type: text/x-csrc
Size: 705 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130905/47d769f1/attachment-0002.c>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: sum_arrayWithout_Pragma.c
Type: text/x-csrc
Size: 824 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130905/47d769f1/attachment-0003.c>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Pragma.png
Type: image/png
Size: 176127 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130905/47d769f1/attachment-0002.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Without_Pragma.png
Type: image/png
Size: 179337 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130905/47d769f1/attachment-0003.png>

Frama-C-discuss mailing list archives

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