--- layout: fc_discuss_archives title: Message 46 from Frama-C-discuss on January 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> </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--