--- layout: fc_discuss_archives title: Message 48 from Frama-C-discuss on March 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Unability to verify an arithmetic assertion disapears in a reduced but similar test case



Hello Virgile,

On Wed, Mar 18, 2009 at 17:54, Virgile Prevosto <virgile.prevosto at cea.fr> wrote:
> if the code of the reduced example is exactly like above, the assertion
> is not proved, since the lack of '@' means that it is not seen as an
> ACSL annotation.

Ohh! I'm ashamed. :-(

> If you put back the '@', there is another issue: the
> assertion is false. Namely, if you call f with n == 0, the loop is not
> entered, and total is still 0 at this point.

Ah yes. I realized that in my larger example that's why I wrote the
following pre-condition.

> Now the larger example has a stronger pre-condition (0<
> num_candidates). So why does alt-ergo still fail on the assertion?
> Well, remember that the only thing that jessie 'knows' after a loop is
> its invariant,

I realized that more or less by trial and error. Is this written
somewhere in Jessie documentation? I have probably read it but
overlooked it.

By the way, I have seen that some "global" knowledge is also kept
(assertions about global variables? function pre-condition?). Is this
correct? Is this described somewhere?

> and here the loop invariant is too weak: it gives an
> upper bound for total, but no lower bound. A possibility (short of the
> ACSL construction \sum which is currently unsupported by jessie) would
> be to add the following invariant:
>
> loop invariant \forall integer j; 0<=j<i ==> total >= counters[j];

Thank you. I'll try that.

I have a side question: I usually write \forall assertions with an
int: "\forall int i; [...]". You write your assertion with "integer",
"\forall integer i; [...]". Is there any difference? Any reason to
prefer one over the other?

Sincerely yours,
david