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]
No subject
- Subject: No subject
- From: bogus@does.not.exist.com ()
- Date: Wed, 28 Jan 2009 17:29:36 -0000
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> </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> </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> </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> </DIV>
<DIV><FONT face=3DArial size=3D2> /*@<BR> =
requires 0=20
<=3D length;<BR> requires \valid_range (a, 0, =
length-1);<BR> requires \valid_range (b, 0,=20
length-1);</FONT></DIV><FONT face=3DArial size=3D2>
<DIV><BR> ensures \result =3D=3D=20
length;<BR> ensures \forall integer k; 0 <=3D =
k <=20
length =3D=3D><BR> (a[k] =3D=3D old_value=20
=3D=3D> b[k] =3D=3D=20
new_value);<BR> ensures \forall integer k; 0 =
<=3D k=20
< length =3D=3D><BR> (a[k] !=3D old_value=20
=3D=3D> b[k] =3D=3D =
a[k]);</DIV>
<DIV> </DIV>
<DIV> */<BR> int replace_copy_array =
(int* a,=20
int length, int* b, int old_value, int new_value =
)<BR>{<BR> =20
int i =3D 0;<BR> /*@<BR> loop =
invariant=20
0 <=3D i <=3D length;</DIV>
<DIV> </DIV>
<DIV> loop invariant \forall integer k; 0 =
<=3D k < i=20
=3D=3D><BR> (a[k] =3D=3D =
old_value=20
=3D=3D><BR> b[k] =3D=3D =
new_value);</DIV>
<DIV> </DIV>
<DIV> loop invariant \forall integer k; 0 <=3D k =
< i=20
=3D=3D><BR> (a[k] !=3D old_value =
=3D=3D><BR> =20
b[k] =3D=3D a[k]);</DIV>
<DIV><BR> */<BR> for (; i !=3D =
length;=20
++i)<BR> =
{<BR> if=20
(a[i]=3D=3Dold_value)<BR> =
=20
b[i] =3D new_value;<BR> =20
else<BR>  =
; b[i]=20
=3D a[i];<BR> }<BR> return =
i;<BR>}</DIV>
<DIV> </DIV>
<DIV>And I have a similar algorithm but this one does not copy the =
result:</DIV>
<DIV> </DIV>
<DIV>/*@<BR> requires 0 <=3D=20
length;<BR> requires \valid_range (a, 0,=20
length-1);</DIV>
<DIV> </DIV>
<DIV> ensures \forall integer=20
k;<BR> 0 <=3D k < =
length=20
=3D=3D><BR> =
(\old(a[k]) =3D=3D=20
old_value =3D=3D><BR> a[k]=3D=3D=20
new_value);<BR> */<BR> void =
replace_array=20
(int* a, int length, int old_value, int new_value =
)<BR>{<BR> =20
int i =3D 0;<BR> /*@<BR> loop =
invariant=20
0 <=3D i <=3D length;</DIV>
<DIV> </DIV>
<DIV> loop invariant \forall integer k; 0 =
<=3D k=20
< i =3D=3D><BR> (\at(a[k],Pre) =
=3D=3D=20
old_value =3D=3D><BR> a[k] =3D=3D =
new_value); <BR> =
*/<BR> for=20
(; i !=3D length; ++i)<BR> =20
{<BR> if (a[i] =3D=3D=20
old_value)<BR> =20
{<BR> =
a[i] =3D=20
new_value;<BR> }</DIV>
<DIV> }<BR>}<BR></DIV>
<DIV>I would like to know, what I have missed.</DIV>
<DIV> </DIV>
<DIV>Thank you for the help,</DIV>
<DIV>Cheers</DIV>
<DIV> </DIV>
<DIV>Christoph</DIV></FONT></BODY></HTML>
------=_NextPart_000_0024_01C99022.B46167A0--
- Prev by Date: [Frama-c-discuss] loop invariant and side effects
- Previous by thread: [Frama-c-discuss] loop invariant and side effects
- Index(es):