# 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] new axiomatic "function"

*Subject*: [Frama-c-discuss] new axiomatic "function"*From*: virgile.prevosto at cea.fr (Virgile Prevosto)*Date*: Mon, 19 Jan 2009 18:06:05 +0100*In-reply-to*: <150B3ED43E794251A80DC6F810A1A019@AHARDPLACE>*References*: <150B3ED43E794251A80DC6F810A1A019@AHARDPLACE>

Hello Christoph, [disclaimer: I'm not sure I've understood the axiomatisation of function_unique_copy. If there's some misinterpretation on my side, please tell me so] Le lun 19 jan 2009 08:49:54 CET, "Christoph Weber" <Christoph.Weber at first.fraunhofer.de> a ?crit : > > I would like to know if something needs to be added to get the proof or if the axiomatization I chose is inconsistent. > > The Function: > > /*@ axiomatic Function_unique_copy { > > logic integer function_unique_copy{La,Lb}(int* a, int* b, integer i_a, integer i_b); > > axiom function_unique_copy_empty{La,Lb}: > \forall int* a, int* b, integer i_a, i_b; > 0 > i_a && 0 > i_b ==> function_unique_copy{La,Lb}(a, b, i_a, i_b) == 0; here, you are saying that function_unique_copy is 0 when both i_a and i_b are strictly negative. I'd say that this is true as soon as one of the lengths is strictly negative (so I'd have 0>i_a || 0 > i_b) > /*@ > requires 0 <= length; > requires \valid_range(a, 0, length-1); > requires \valid_range(dest, 0, length-1); > > ensures 0 <= \result <= length; > > ensures \result == function_unique_copy{Old,Here}(a, dest, length-1, \result-1); > */ > > int unique_copy_array(int* a, int length, int* dest) > { > > int i_a = 0; > int i_dest = 0; > > if (length == 0) > return i_dest; > > int value = a[i_a]; > dest[i_dest] = value; > i_a++; > Without i_dest++ here, you'll be overwriting the first element of dest with the first a[i_a] distinct from a[0]. This is consistent with your axiomatisation, as function_unique_copy(i_a,i_b,0,0) returns 1 regardless of the values of i_a[0] and i_b[0], but I'm unsure that this is the intended behavior. > /*@ > loop invariant 0 < i_a <= length; > loop invariant i_dest < i_a; > loop invariant 0 <= i_dest < length; > > loop invariant i_dest == function_unique_copy{Pre,Here}(a, dest, i_a-1, i_dest-1); > */ in the invariant, you do not specify anything about the variable value, so that the verification condition generator can't do much with it. Possible invariants are: loop invariant a[i_a-1] == value; loop invariant i_dest !=0 ==> dest[i_dest-1] == value ; Note that the guard i_dest !=0 is here because of the special role of the dest[0] cell, which will hold successively a[0] and a[i_a] where i_a is the smallest index such that a[0] != a[i_a] > while (i_a != length) > { > if (!(value == a[i_a])) > { > value = a[i_a]; > dest[i_dest] = value; Apparently Z3 is smart enough to use only the original assertion, but alt-ergo and Simplify need some help here (again, the case where i_dest is 0 is a bit special) /*@ assert i_dest == function_unique_copy{Pre,Here}(a,dest,i_a-1,i_dest-1); */ /*@ assert a[i_a] != a[i_a-1] && i_dest!=0 ==> dest[i_dest]!=dest[i_dest-1]; */ > /*@assert > i_dest+1==function_unique_copy{Pre,Here}(a,dest,i_a,i_dest); > */ > ++i_dest; > } > > > i_a++; > } I'm unsure of this ++i_dest. In fact i_dest itself meets the post-condition, not its successor. Could it be related to the fact that i_dest is not incremented before entering the loop? > return ++i_dest; > } > -- Virgile Prevosto Ing?nieur-Chercheur, CEA, LIST Laboratoire de S?ret? des Logiciels +33/0 1 69 08 71 83

**Follow-Ups**:**[Frama-c-discuss] new axiomatic "function"***From:*Christoph.Weber at first.fraunhofer.de (Christoph Weber)

**References**:**[Frama-c-discuss] new axiomatic "function"***From:*Christoph.Weber at first.fraunhofer.de (Christoph Weber)

- Prev by Date:
**[Frama-c-discuss] perhaps a bug** - Next by Date:
**[Frama-c-discuss] new axiomatic "function"** - Previous by thread:
**[Frama-c-discuss] new axiomatic "function"** - Next by thread:
**[Frama-c-discuss] new axiomatic "function"** - Index(es):