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