--- layout: fc_discuss_archives title: Message 109 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 tried to complete the specification of the same source code
(attached).

After inserting the two annotations below, there were some not proved VCs
(401/405):
assigns Gbl_Eventos[9].Gbl_Ativo;
ensures (pri == 1) && (ID == 1) && (\old(Eventos[9].Ativo) == 0) && average
> 12.0 ==> Eventos[9].Ativo == 1;

In order to write this postcondition we followed the sequence of the
statements in the source code.

What is wrong with these annotations?

Best regards,
Nanci, Luciana, Rovedy



2013/9/14 Claude Marche <Claude.Marche at inria.fr>

>
>
> On 09/12/2013 08:06 PM, Rovedy Aparecida Busquim e Silva wrote:
> > 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?
>
> the lemma says the if some integer n is less or equal 3, then when
> converting it to a rel number the result is less or equal 3.0. Seems
> stupid but needed to help provers...
>
> > 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?
>
> It should not make any major difference. However since the context of
> the VC would be a bit different (e.g. not the same order of hypotheses),
> you may need to increase a little the time limit given to the prover.
>
> I tried your example and I've been abble to prove it, both in case j is
> global and when it is local. Although, I needed to modify a bit the
> annotations: removing the "loop assigns p,j" that disturbs Jessie, and
> replacing "sum(x,...)" by "sum(x+0,...)" because it is refused by
> Frama-C kernel. I'm using Frama-C Fluorine 20130601 + Why 2.33 + Why3 +
> provers Alt-Ergo, CVC3 and Gappa.
>
> Hope this helps,
>
> - Claude
>
>
> > 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
> >>
> >>
> >> _______________________________________________
> >> 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
>
> _______________________________________________
> 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/20130916/444c2731/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: site003_53.c
Type: text/x-csrc
Size: 2879 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130916/444c2731/attachment.c>