--- layout: fc_discuss_archives title: Message 34 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



Hallo Christoph,

Le mer 10 d?c 2008 13:58:59 CET,
"Christoph Weber" <Christoph.Weber at first.fraunhofer.de> a ?crit :

> 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.
> 

That's not normal. Can you be more specific about the troubles you have
with using a variable called null (and which frama-c version you're
using)? The current development version seems to be fine with this
respect.

> /*@
> 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.

I guess the problem lies in the invariant for index_b, which is too
weak. Namely, if you start a loop step with index_b == length_b (which
is fine as far as the invariant is concerned), you might increment
index_b, and thus, since you return only in the case where index_b and
length_b are equal, you end up with index_b > length_b at the next
step, so that the invariant is broken. It is thus a good point for
jessie that you can not prove it. 

Note that there is no issue with index_a since the equality test with
length_a occurs before the incrementation.

A loop invariant 0 <= index_b < length_b would be better, but for that
you need to require that length_b > 0 (otherwise the invariant might
not hold at the beginning of the loop).

> 3. An other algorithm I defined uses two for-loops:

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

I have to admit that I haven't looked to closely at your specification,
but it usually helps to provide some assertions inside the loop.

-- 
E tutto per oggi, a la prossima volta.
Virgile