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

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



Hi,

We have run the example as suggested by Claude
(http://proval.lri.fr/gallery/ScalarProduct.en.html).

We used the example annotations in our code (attached) and the all VCs
were proved.

However, we have some doubts:

1. We have used the lemma bound_int_to_real but we did not understand
how it works.
Why the define NMAXR is used?

2. The variable j used in the loop was global in the legacy source
code. However, the loop invariant  was not proved (loop invariant
\abs(p - sum(x,j)) <= j * BOUND).
  We changed the variable j to local and the loop invariant was proved.
  Does not the loop invariant work with global variable?

Best regards,
Nanci, Luciana e Rovedy




2013/9/7 Claude Marche <Claude.Marche at inria.fr>
>
>
>
> On 09/07/2013 10:56 AM, Claude Marche wrote:
>>>
>>> Alternatively, you can force the computation into float in sum
>>> by modifying your axiom:
>>>    @   axiom sum2{L} :
>>>    @     \forall float *t, integer i, j;
>>>    @       sum(t,i,j+1) == (float)(sum(t,i,j) + t[j]);
>>> But this is not a very good idea IMHO: as floating point addition is
>
>
> A very bad idea indeed.
>
> - 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 --------------
A non-text attachment was scrubbed...
Name: site003_43.c
Type: text/x-csrc
Size: 2255 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130912/a035966a/attachment.c>