--- layout: fc_discuss_archives title: Message 57 from Frama-C-discuss on April 2012 ---
Dear Nicolas, You made several beginner's mistakes in the specification of your C code. I'd like to recommend the reading of a few documents to help you find the adequate annotations. These are listed on the Jessie web page: http://krakatoa.lri.fr/#jessie. Additionally, for more general background on deductive verification, as Jessie and WP plug-ins do, you may have a look at new lecture notes available at http://www.lri.fr/~marche/MPRI-2-36-1/ Let me now comment you annotated code in details. ---------------------------- float abs(float i) { if (i< 0.0) return -i; return i; } ---------------------------- A basic fact about deductive verification: it is modular, it proceeds function by function. You need to put a contract on this function if you want to prove something when you call it. An adequate contract could be assigns \nothing; ensures \result == \abs(i) ------------------------------------- /*@ requires (-25.0<= A<= 25.0); requires (-53.5<= B<= 53.5); */ float main(float A, float B){ int i,j,k; float x,y; //float C = Frama_C_float_interval(-25.0,25.0); /*@ loop invariant (0 == i)&& (i< 51); loop assigns i; loop variant (51-i); */ for(i=0; i<51; i++) { ----------------------------------- As David Mentr? already said, (0 == i)&& (i< 51) is not a proper invariant, Moreover, did you noticed that it is logically equivalent to i == 0 ? 0<= i<= 52 is indeed the proper loop invariant. --------------------------------- A=(-25.0+i); //@ assert (A == (-25.0+i)); } ------------------------------ I really wonder what you want to prove here. Such an assertion is indeed meaningfull since it amounts to prove that the computation of -25.0+i is exact. I would guess that Gappa is able to prove such an assertion, although it is far for trivial. But if you real intention is to prove something about the value of A after the loop, then you should state that also as a loop invariant, something like loop invariant i> 0 ==> A == -25.0 + i - 1 (It's complicated, but your program is not very natural anyway...) Then if you like you could also add, after the loop, assert A == 26.0 --------------------------------------------------- /*@ loop invariant (0 == j)&& (j< 108); loop assigns j; loop variant (108-j); */ for(j=0; j<108; j++) { B=(-53.5+j); //@ assert (B == (-53.5+j)); } ------------------------------------- Similar remarks as the previous loop assert B == 54.5 should be provable (please forbid any mistake in my calculations by brain) ------------------------------- /*@ loop invariant (0 == k< 108); loop assigns k; loop variant (108-k); */ for(k=0; k<108;k++) ----------------------------- Again a wrong loop invariant ---------------------------- { x = abs(A-B); if (x< 0) x = -x; ----------------- surprising statement here, since x should already be non-negative... -------------------- //@ assert (x>=0); ---------- ... but to prove it you need a contract on function "abs" ----------------------------- //@ assert (7< x< 28.5); --------------------------- for me x = 28.5, so it should be wrong. Please be carefule about your use of "<" versus"<=". But as David Mentr? said: since you put a wrong loop invariant, your are trying to prove this is an inconsistant context, hence everything get the valid status. -------------------------------- y = abs(B-A); if (y< 0) y = -y; //@ assert (y>=0); //@ assert (7< y< 28.5); } --------------------------------- wrong again ----------------------- //@ assert (x == y); ---------------------- should be provable, if there is a contract on function "abs" ----------------------- return x; return y; } ---------------------------- Hope this helps, - Claude