--- layout: fc_discuss_archives title: Message 57 from Frama-C-discuss on April 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] similar assertions not all validated



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