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] further problem-reports

  • Subject: [Frama-c-discuss] further problem-reports
  • From: Christoph.Weber at first.fraunhofer.de (Christoph Weber)
  • Date: Wed, 10 Dec 2008 13:58:59 +0100
Hello again,

I would like to report some other things I came across and ask some questions as well:

1. while exploring axiomatic definitions I discovered, defining a variable "null" causes Problems, obviously it interferes with the "\null" but I would like to be able to use "null" nevertheless.

2. I have an includes algorithm:

It returns a "true" if all the elements of range "b" are present in range "a" with exactly the same quantity.

/*@
predicate ascending_array{Here}(int* a, integer length) =
\forall integer k1, k2;
0 <= k1 <= k2 < length ==> a[k1] <= a[k2];
*/
/*@
    requires 0 <= length_a;
    requires 0 <= length_b;
    requires \valid_range (a, 0, length_a);
    requires \valid_range (b, 0, length_b);
    requires ascending_array(a, length_a);
    requires ascending_array(b, length_b);

    ensures \forall integer k2; \exists integer k1; 0 <= k2 < length_b && 0 <= k1 < length_a
        ==> nb_occ(b, 0, length_b, b[k2]) == nb_occ(a, 0, length_a, a[k1]);
*/
int includes_array(int* a , int length_a , int* b, int length_b )
{
int index_a = 0;
int index_b = 0;
/*@
loop invariant 0 <= index_a <= length_a;
loop invariant 0 <= index_b <= length_b;
loop invariant \forall integer k2; \exists integer k1;

0 <= k2 < index_b && 0 <= k1 < index_a ==>
nb_occ(b, 0, index_b, b[k2]) == nb_occ(a, 0, index_a, a[k1]);
*/
while (index_a != length_a)
{
if (b[index_b] < a[index_a])
break;
else if (a[index_a] < b[index_b])
++index_a;
else
{
++index_a;
++index_b;
}
if (index_b == length_b) return 1;
}
return 0;
}

I understand that nb_occ might cause the solver  the same problems, it caused in the remove_copy algorithm.

But I don't understand, why 
loop invariant 0 <= index_a <= length_a;
loop invariant 0 <= index_b <= length_b;
wont get proven.


3. An other algorithm I defined uses two for-loops:
find_first_of_array returns an index to the first element in the range "a", that is equal to some element in range "b":


/*@
requires 0 <= length_a;
requires 0 <= length_b;
requires \valid_range (a, 0, length_a);
requires \valid_range (b, 0, length_b);
ensures 0 <= \result <= length_a;
ensures \exists integer k2; \forall integer k1; 0 <= k1 < \result && 0 <= k2 < length_b ==>
a[k1] != a[k2];
behavior found:
ensures \exists integer k1, k2; 0 <= k1 < length_a && 0 <= k2 < length_b ==>
a[\result] == a[k1] == b[k2];

*/
int find_first_of_array (int* a, int length_a, int* b, int length_b)
{
int index_a = 0;
int index_b = 0;
/*@
loop invariant 0 <= index_a <= length_a;
loop invariant 0 <= index_b <= length_b;
loop invariant \forall integer k1; \exists integer k2; 0 <= k1 < index_a && 0 <= k2 < index_b ==>
a[k1] != a[k2];
for found:
loop invariant \forall integer k1, k2; 0 <= k1 < index_a && 0 <= k2 < index_b ==> a[k1] != b[k2];
*/
for ( ; index_a != length_a; ++index_a )
{
index_b = 0;
/*@
loop invariant 0 <= index_a <= length_a;
loop invariant 0 <= index_b <= length_b;
loop invariant \exists integer k2; \forall integer k1; 0 <= k1 < index_a && 0 <= k2 < index_b ==>
a[k1] != a[k2];
for found:
loop invariant \forall integer k1, k2; 0 <= k1 < index_a && 0 <= k2 < index_b ==> a[k1] != b[k2];
*/
for (; index_b != length_b; ++index_b)
if (b[index_b] == a[index_a])
return index_a;
}
return length_a;
}

I would like to know, what can be done to help the proover to master the difficult quantified expressions.


Cheers 
Christoph
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081210/06f9a92c/attachment.htm