No subject


Wed Jan 28 18:29:36 CET 2009


write on the same memory location and to prove something about it.
(Please correct me if I am wrong)

I have an annotated algorithm that is proven:

 /*@
     requires 0 <=3D length;
     requires \valid_range (a, 0, length-1);
     requires \valid_range (b, 0, length-1);

     ensures \result =3D=3D length;
     ensures \forall integer k; 0 <=3D k < length =3D=3D>
     (a[k] =3D=3D old_value =3D=3D>        b[k] =3D=3D new_value);
     ensures \forall integer k; 0 <=3D k < length =3D=3D>
     (a[k] !=3D old_value =3D=3D>        b[k] =3D=3D a[k]);

    */
    int replace_copy_array (int* a, int length, int* b, int old_value, =
int new_value )
{
    int i =3D 0;
    /*@
     loop invariant 0 <=3D i <=3D length;

     loop invariant \forall integer k; 0 <=3D k < i =3D=3D>
        (a[k] =3D=3D old_value =3D=3D>
        b[k] =3D=3D new_value);

    loop invariant \forall integer k; 0 <=3D k < i =3D=3D>
    (a[k] !=3D old_value =3D=3D>
    b[k] =3D=3D a[k]);

    */
    for (; i !=3D length; ++i)
    {
        if (a[i]=3D=3Dold_value)
            b[i] =3D new_value;
        else
            b[i] =3D a[i];
    }
    return i;
}

And I have a similar algorithm but this one does not copy the result:

/*@
     requires 0 <=3D length;
     requires \valid_range (a, 0, length-1);

     ensures \forall integer k;
         0 <=3D k < length =3D=3D>
         (\old(a[k]) =3D=3D old_value =3D=3D>
       a[k]=3D=3D new_value);
    */
    void replace_array (int* a, int length, int old_value, int new_value =
)
{
    int i =3D 0;
    /*@
     loop invariant 0  <=3D i <=3D length;

     loop invariant \forall integer k;  0 <=3D k < i =3D=3D>
       (\at(a[k],Pre) =3D=3D old_value =3D=3D>
       a[k] =3D=3D new_value);  =20
    */
    for (; i !=3D length; ++i)
    {
        if (a[i] =3D=3D old_value)
        {
            a[i] =3D new_value;
        }
    }
}

I would like to know, what I have missed.

Thank you for the help,
Cheers

Christoph
------=_NextPart_000_0024_01C99022.B46167A0
Content-Type: text/html;
	charset="iso-8859-1"
Content-Transfer-Encoding: quoted-printable

<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
<HTML><HEAD>
<META http-equiv=3DContent-Type content=3D"text/html; =
charset=3Diso-8859-1">
<META content=3D"MSHTML 6.00.6001.18203" name=3DGENERATOR>
<STYLE></STYLE>
</HEAD>
<BODY bgColor=3D#ffffff>
<DIV><FONT face=3DArial size=3D2>Hello,</FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT>&nbsp;</DIV>
<DIV><FONT face=3DArial size=3D2>I am trying to explore the limitations =
of proving=20
with Jessie.</FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT>&nbsp;</DIV>
<DIV><FONT face=3DArial size=3D2>From what I understood of the recent =
mails, it is=20
difficult to read and write on the same memory location and to prove =
something=20
about it.</FONT></DIV>
<DIV><FONT face=3DArial size=3D2>(Please correct me if I am =
wrong)</FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT>&nbsp;</DIV>
<DIV><FONT face=3DArial size=3D2>I have an annotated algorithm that is=20
proven:</FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT>&nbsp;</DIV>
<DIV><FONT face=3DArial size=3D2>&nbsp;/*@<BR>&nbsp;&nbsp;&nbsp;&nbsp; =
requires 0=20
&lt;=3D length;<BR>&nbsp;&nbsp;&nbsp;&nbsp; requires \valid_range (a, 0, =

length-1);<BR>&nbsp;&nbsp;&nbsp;&nbsp; requires \valid_range (b, 0,=20
length-1);</FONT></DIV><FONT face=3DArial size=3D2>
<DIV><BR>&nbsp;&nbsp;&nbsp;&nbsp; ensures \result =3D=3D=20
length;<BR>&nbsp;&nbsp;&nbsp;&nbsp; ensures \forall integer k; 0 &lt;=3D =
k &lt;=20
length =3D=3D&gt;<BR>&nbsp;&nbsp;&nbsp;&nbsp; (a[k] =3D=3D old_value=20
=3D=3D&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; b[k] =3D=3D=20
new_value);<BR>&nbsp;&nbsp;&nbsp;&nbsp; ensures \forall integer k; 0 =
&lt;=3D k=20
&lt; length =3D=3D&gt;<BR>&nbsp;&nbsp;&nbsp;&nbsp; (a[k] !=3D old_value=20
=3D=3D&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; b[k] =3D=3D =
a[k]);</DIV>
<DIV>&nbsp;</DIV>
<DIV>&nbsp;&nbsp;&nbsp; */<BR>&nbsp;&nbsp;&nbsp; int replace_copy_array =
(int* a,=20
int length, int* b, int old_value, int new_value =
)<BR>{<BR>&nbsp;&nbsp;&nbsp;=20
int i =3D 0;<BR>&nbsp;&nbsp;&nbsp; /*@<BR>&nbsp;&nbsp;&nbsp;&nbsp; loop =
invariant=20
0 &lt;=3D i &lt;=3D length;</DIV>
<DIV>&nbsp;</DIV>
<DIV>&nbsp;&nbsp;&nbsp;&nbsp; loop invariant \forall integer k; 0 =
&lt;=3D k &lt; i=20
=3D=3D&gt;<BR>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;  (a[k] =3D=3D =
old_value=20
=3D=3D&gt;<BR>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;  b[k] =3D=3D =
new_value);</DIV>
<DIV>&nbsp;</DIV>
<DIV>&nbsp;&nbsp;&nbsp; loop invariant \forall integer k; 0 &lt;=3D k =
&lt; i=20
=3D=3D&gt;<BR>&nbsp;&nbsp;&nbsp; (a[k] !=3D old_value =
=3D=3D&gt;<BR>&nbsp;&nbsp;&nbsp;=20
b[k] =3D=3D a[k]);</DIV>
<DIV><BR>&nbsp;&nbsp;&nbsp; */<BR>&nbsp;&nbsp;&nbsp; for (; i !=3D =
length;=20
++i)<BR>&nbsp;&nbsp;&nbsp; =
{<BR>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; if=20
(a[i]=3D=3Dold_value)<BR>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=
&nbsp;&nbsp;&nbsp;=20
b[i] =3D new_value;<BR>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=20
else<BR>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp=
; b[i]=20
=3D a[i];<BR>&nbsp;&nbsp;&nbsp; }<BR>&nbsp;&nbsp;&nbsp; return =
i;<BR>}</DIV>
<DIV>&nbsp;</DIV>
<DIV>And I have a similar algorithm but this one does not copy the =
result:</DIV>
<DIV>&nbsp;</DIV>
<DIV>/*@<BR>&nbsp;&nbsp;&nbsp;&nbsp; requires 0 &lt;=3D=20
length;<BR>&nbsp;&nbsp;&nbsp;&nbsp; requires \valid_range (a, 0,=20
length-1);</DIV>
<DIV>&nbsp;</DIV>
<DIV>&nbsp;&nbsp;&nbsp;&nbsp; ensures \forall integer=20
k;<BR>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; 0 &lt;=3D k &lt; =
length=20
=3D=3D&gt;<BR>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; =
(\old(a[k]) =3D=3D=20
old_value =3D=3D&gt;<BR>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; a[k]=3D=3D=20
new_value);<BR>&nbsp;&nbsp;&nbsp; */<BR>&nbsp;&nbsp;&nbsp; void =
replace_array=20
(int* a, int length, int old_value, int new_value =
)<BR>{<BR>&nbsp;&nbsp;&nbsp;=20
int i =3D 0;<BR>&nbsp;&nbsp;&nbsp; /*@<BR>&nbsp;&nbsp;&nbsp;&nbsp; loop =
invariant=20
0&nbsp; &lt;=3D i &lt;=3D length;</DIV>
<DIV>&nbsp;</DIV>
<DIV>&nbsp;&nbsp;&nbsp;&nbsp; loop invariant \forall integer k;&nbsp; 0 =
&lt;=3D k=20
&lt; i =3D=3D&gt;<BR>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (\at(a[k],Pre) =
=3D=3D=20
old_value =3D=3D&gt;<BR>&nbsp;&nbsp;&nbsp;&nbsp; &nbsp;&nbsp;a[k] =3D=3D =

new_value);&nbsp;&nbsp;&nbsp;<BR>&nbsp;&nbsp;&nbsp; =
*/<BR>&nbsp;&nbsp;&nbsp; for=20
(; i !=3D length; ++i)<BR>&nbsp;&nbsp;&nbsp;=20
{<BR>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; if (a[i] =3D=3D=20
old_value)<BR>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=20
{<BR>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; =
a[i] =3D=20
new_value;<BR>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; }</DIV>
<DIV>&nbsp;&nbsp;&nbsp; }<BR>}<BR></DIV>
<DIV>I would like to know, what I have missed.</DIV>
<DIV>&nbsp;</DIV>
<DIV>Thank you&nbsp;for the help,</DIV>
<DIV>Cheers</DIV>
<DIV>&nbsp;</DIV>
<DIV>Christoph</DIV></FONT></BODY></HTML>

------=_NextPart_000_0024_01C99022.B46167A0--




More information about the Frama-c-discuss mailing list