# 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] similar assertions not all validated

*Subject*: [Frama-c-discuss] similar assertions not all validated*From*: Claude.Marche at inria.fr (Claude Marche)*Date*: Wed, 18 Apr 2012 07:27:07 +0200*In-reply-to*: <0627805BEE18C14981A31E75C2452AA123AD5E490A@Y000IMRV02.rd1.rf1>*References*: <0627805BEE18C14981A31E75C2452AA123AD5E490A@Y000IMRV02.rd1.rf1>

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

**References**:**[Frama-c-discuss] similar assertions not all validated***From:*nicolas.muller at sagem.com (MULLER Nicolas (SAGEM DEFENSE SECURITE))

- Prev by Date:
**[Frama-c-discuss] examples of linked lists or trees** - Next by Date:
**[Frama-c-discuss] similar assertions not all validated** - Previous by thread:
**[Frama-c-discuss] similar assertions not all validated** - Next by thread:
**[Frama-c-discuss] examples of linked lists or trees** - Index(es):