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

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



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>