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

[Frama-c-discuss] further problem-reports



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