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] proof of logic expression

  • Subject: [Frama-c-discuss] proof of logic expression
  • From: Christoph.Weber at first.fraunhofer.de (Christoph Weber)
  • Date: Thu, 18 Dec 2008 08:38:01 +0100
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