# 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*: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)*Date*: Thu, 5 Sep 2013 10:27:16 -0300*In-reply-to*: <5216629A.5080303@inria.fr>*References*: <CAEtoXR21n9RPnwGE_UQ7zDjqrNPjhhRMuG5kQdzM=SjH7z+9CA@mail.gmail.com> <52162B8A.4080703@inria.fr> <CAEtoXR2DsVLvtKZM9PiFNPxx-=w11eY0sr2WNQ4ymdv74P-h4A@mail.gmail.com> <5216629A.5080303@inria.fr>

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>

**Follow-Ups**:**[Frama-c-discuss] [Jessie] loop invariant***From:*virgile.prevosto at m4x.org (Virgile Prevosto)

- Prev by Date:
**[Frama-c-discuss] Introductory slides on Frama-C** - Next by Date:
**[Frama-c-discuss] How would one annotate a function in an external header?** - Previous by thread:
**[Frama-c-discuss] Issues with WP on program doing simplepointer arithmetic** - Next by thread:
**[Frama-c-discuss] [Jessie] loop invariant** - Index(es):