--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on February 2013 ---
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>