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] Loop invariants with imbricated loops.

  • Subject: [Frama-c-discuss] Loop invariants with imbricated loops.
  • From: dragan.stosic at gmail.com (Dragan)
  • Date: Wed, 20 May 2009 17:39:17 +0100
  • In-reply-to: <20090520172521.62f22af3@is005115>
  • References: <4A1402E9.8090307@fr.thalesgroup.com> <20090520172521.62f22af3@is005115>
Hi all
I am new in community.
If someone has problem with Ubuntu Z3 installation I have solution:
1) download z3-1.3.6.msi Latest version: Z3
1.3<http://research.microsoft.com/research/downloads/details/0a7db466-c2d7-4c51-8246-07e25900c7e7/details.aspx>
.
2) open with wine and install
3) create your home/user/bin directory
4) in .bashrc add : export PATH=/home/user/bin:$PATH
5) restart session
6)in home/user/bin add file z3  with content

    wine
/home/dragan/.wine/drive_c/Program_Files/Microsoft_Research/Z3-1.3.6/bin/z3.exe
/s $*

7)save and change permission
8)sudo chmod 775 z3
9) why-config

starting autodetection...
Found prover Alt-Ergo version 0.8
Found prover Simplify version 1.5.4
err:winedevice:ServiceMain driver L"vstor2-ws60" failed to load
Found prover Z3 version 1.3
Found prover Yices version 1.0.21
Found prover CVC3 version devel
Found prover Coq version 8.1pl3
detection done.
writing rc file...

all other provers you can set-up on similar way

after running frama-c -jessie-analysis -jessie-gui file.c
you will see all available provers.

Also two question.
In frama-c/why directory I found why-2.17.
It is not clear to me ...?
Why  we have two " why " version ?
Another question: Is it possible somehow to include escJava2 prover in
frama-c why environment?
Best Regards
Dragan
Senior Software Developer
UCD_CASL



On Wed, May 20, 2009 at 4:25 PM, Virgile Prevosto
<virgile.prevosto at cea.fr>wrote:

> Le mer. 20 mai 2009 15:17:29 CEST,
> JENN Eric <eric.jenn at fr.thalesgroup.com> a ?crit :
>
> > Me, again.
> > Consider the following code:
> >
> > void test1() {
>
> //...
>
> >   {
> >     /*@ loop invariant 0 <= b <= 3;
> >         loop invariant
> >       \forall integer j;
> >         ( 0 <= j < b ) ==> (the_array[a+j*3] == -1);
> >       @*/
> >     for ( b = 0; b< 3 ; b++)
> >     {
> >       the_array[a+b*3] = -1;
> >     }
> >
> >     /*@
> >       assert
> >       \forall integer j;
> >             ( 0 <= j < 3 ) ==> (the_array[a+j*3] == -1);
> >         @*/
> >   }
> > }
> >
> > All POs corresponding to the invariants of the inner-most loop, and the
> assertion, are discharged.
> > The PO corresponding to the preservation of invariant of the outer-most
> is demonstrated not to be valid... and I don't understand why?
>
> Because, the loop invariant of the inner loop is too weak: you specify
> what happens on the a-th 'column' of the array, but not that the
> preceding ones are left untouched by the loop. And since the loop
> annotation is the only thing that jessie sees outside of the loop,
> there is nothing in the hypotheses of the PO that says that these
> 'columns' still contain -1.
> Now the standard ACSL way of specifying that would be a via loop assigns
> (left as an exercise for the reader). However, since loop assigns are
> not handled by the current version of the jessie plugin, a work-around
> must be found in the form of another invariant:
>        loop invariant
>        \forall integer i,j;
>        (0<=i <a) && (0<=j<3) ==> the_array[i+j*3] == -1;
>
> > In particular, the assertion is demonstrated to be  TRUE for all a in
> [0,3[ so, doesn't this guarantee the preservation of the outer-most
> invariant?
>
> No, for the same reason as above: the assertion talks about the a-th
> 'column'.
>
> As a final note, note that the outer loop invariant seem to be handled
> more easily by ATP when it is written in this form:
>     loop invariant
>      \forall integer i,j;
>        ( 0 <= i < a ) && (0<=j<3) ==>
>           (the_array[i+j*3] == -1);
>
> Best regards,
> --
> E tutto per oggi, a la prossima volta.
> Virgile
>
>
> _______________________________________________
> 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/20090520/a114e1c8/attachment.htm