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 preserved

  • Subject: [Frama-c-discuss] Jessie - loop invariant preserved
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
  • Date: Fri, 8 Feb 2013 16:35:23 -0200
Hello,

I am learning about Jessie plugin with a simple example (source code
attached).

I have perfomed the verification according to Jessie Manual. First, I have
done the safety verification (using pragmas) and, after that, the
functional verification.

Actually, I have received a answer from list that helped me (
http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2012-November/003444.html
).

However, I didnt get to prove the function.

When I started to think in functional verification, my first action was to
write a pos-condition.

Then, I didn?t get prove and I inserted a loop invariant that is equal to
pos-condition.

In this case, the pos condition was proved but the Vc related with the
"loop invariant preserved" not.

My doubts are:

1) Is my pos-condition written correctly? Would I write an annotation
similar to if statement?

2) In this function, there is only a loop. So, the pos-condition is equal
to loop invariant, is this right?

3) How I do to prove this kind of VC "loop invariant preserved"?


Thanks a lot!
Best regards,
Rovedy

//-------------------------------------------------------------------------------------------------------------------------------------------------------
float Tempo;
#define FALSE 0
#define TRUE 1

struct
{
      unsigned int G_Ativo :1,
             G_Tratado :1;
float G_Inst_Ativ;
} G_E[5];


/*@
@ ensures  \forall integer i; 0<=i<5 ==> (G_E[i].G_Inst_Ativ <= Tempo ==>
G_E[i].G_Ativo == 1);
@ */
void test(void)
{
int i = 0;
 /*@
  loop invariant  0 <= i <=5;
  loop invariant \forall integer i; 0<=i<5 ==>   (G_E[i].G_Inst_Ativ <=
Tempo ==> G_E[i].G_Ativo == 1);
  loop variant 5 - i;
 */
  for(i=0;i<5;i++)
  {
     if(G_E[i].G_Ativo == FALSE && G_E[i].G_Inst_Ativ <= Tempo)
     {
        G_E[i].G_Ativo = TRUE;
     }
  }
}
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130208/4a736ae9/attachment-0001.html>