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: virgile.prevosto at cea.fr (Virgile Prevosto)
  • Date: Fri, 12 Dec 2008 17:53:54 +0100
  • In-reply-to: <44B7146D318245348439B9D5D5BDAA17@AHARDPLACE>
  • References: <44B7146D318245348439B9D5D5BDAA17@AHARDPLACE>
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