--- layout: fc_discuss_archives title: Message 56 from Frama-C-discuss on December 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] proof of logic expression



Hello again, and thank you for the continuing help.


Regardless of the code, I want to proof a postcondition for a remove_copy algorithm:

int remove_copy_array (int* a, int length, int* dest, int value )
{
int index_a = 0;
int index_dest = 0;

for ( ; index_a != length; ++index_a) 
if (a[index_a] != value)
{
dest[index_dest] = a[index_a];
++index_dest; 
}
return index_dest;
}

This algorithm copies every element from range a to range dest.

So far i can proof that  value does not appear in dest:
ensures \forall integer k; 0 <= k < \result ==> dest[k] != value;

And that \result (==length of the dest-range) is equal to the length of the range a minus the number of occurrences of value:
ensures \result == length - nb_occ{Old}(a, 0, length-1, value);


What I want to proof now, is that all the other elements from range a have been copied to range dest. Since multiple occurrences of the same element are allowed, a simple "check" via an \exists-quantifier is not sufficient. I also have to proof, that the number of equal elements in both arrays are equal.

I can proof, that at least one occurence has been copied:
ensures \forall integer m; 0 <= m < \result ==> ( \exists integer n; 0 <= n < length &&
dest[m] == a[n] );


But if I try to proof the equivalence of occurences of equal elements, I get problems:
ensures \forall integer m; 0 <= m < \result ==> ( \exists integer n; 0 <= n < length &&
(dest[m] == a[n] ==> nb_occ{Here}(dest, 0, \result-1, dest[m]) == nb_occ{Old}(a, 0, length-1, a[n])));

I believe, that dest[m] and a[n] can differ in each iteration and therefore it is not possible to get a consistent loop invariant.
To get something like this to work, I would need to span a tree for every possible element and "count" the depth.
I dont't believe that this works.

What I would like to know is, if there is a possibility to formulate what i intent.

By the way:

/*@ axiomatic NbOcc {

logic integer nb_occ{L}(int* a, integer _null, integer index, int value);
axiom nb_occ_empty{L}:
    \forall int* a, int value, integer _null, index; _null > index ==> nb_occ(a,_null,index,value) == 0;
axiom nb_occ_true{L}:
    \forall int* a, int value, integer _null, index; _null <= index && a[index] == value ==> 
    nb_occ(a,_null,index,value) == nb_occ(a,_null,index-1,value) + 1;
axiom nb_occ_false{L}:
    \forall int* a, int value, integer _null, index; _null <= index && a[index] != value ==> 
    nb_occ(a,_null,index,value) == nb_occ(a,_null,index-1,value);
}
*/

Cheers

Christoph
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081218/c356b438/attachment-0001.htm