Frama-C-discuss mailing list archives

yannick.moy at gmail.com (Yannick Moy) · Mon Nov 3 15:17:26 2008

Hello,

Existing solutions for recursively defined logic functions were not
satisfying:

- recursive logic function may very easily be ill-defined, in particular
when they should be defined only for some arguments, and left unspecified
for others (e.g., the length of a list), leading to inconsistencies.
For example, the following "natural" definition is wrong:

//@ logic integer list_length(List *x) = (x == NULL) ? 0 :
list_length(x->next) + 1;

By examining the case where x == x->next, it is possible to deduce that 0 ==
1.

- reads clauses are likewise easily ill-written, leading to other
inconsistencies with axioms defining the function.
For example, the following reads clause is wrong:

//@ logic integer list_length(List *x) read x, x->next;

This does not take into account x->next->next, etc.

Our solution is to group together the declaration of a logic function
together with axioms that define it, in a axiomatic. Then, the reads clause
is automatically inferred from axioms. This is what is done for NbOcc
axiomatic, around nb_occ logic function. The same is true for predicates, or
various logic functions and predicates defined by a set of axioms.

HTH,
Yannick

On Mon, Nov 3, 2008 at 2:51 PM, Christoph Weber <
Christoph.Weber@first.fraunhofer.de> wrote:

>  Thanks for the example, that helps a lot. Funny that you discovered an
> error, I wasn't even aware of it :).
>
> I realize that the given axiomatic predicate will work. My Problem is
> why???
> Don't I have to define a function body or something like it and
> how will it be processed?
> In some examples I came across a reads[] clause, is this necessary or what
> does it do?
>
> You see I am confused.
>
> Cheers
> Christoph
>
>
> ----- Original Message -----
> *From:* Yannick Moy <yannick.moy@gmail.com>
> *To:* Christoph Weber <Christoph.Weber@first.fraunhofer.de>
> *Cc:* frama-c-discuss@lists.gforge.inria.fr
> *Sent:* Monday, November 03, 2008 2:16 PM
> *Subject:* Re: [Frama-c-discuss] Axiomatic Definitions
>
> Hi,
>
> You were right, there is indeed a typo in the version of NbOcc axiomatic
> present in ACSL manual ("i" is used twice where "j" is expected). The file
> in attachment is a correct version of NbOcc axiomatic as well as a counting
> C function that expresses such a property in its loop invariant and
> postcondition. All 4 of Alt-Ergo, Simplify, Z3 and Yices completely prove
> the generated VC.
>
> As I said, there are some issues with our memory model in the Jessie plugin
> that I cannot decide alone, therefore we must delay an answer to your
> previous mail to wednesday or thursday, depending on when we finally can
> meet to discuss this problem. Sorry for this inconvenience.
>
> Best regards,
>
> Yannick
>
>
> On Mon, Nov 3, 2008 at 1:06 PM, Christoph Weber <
> Christoph.Weber@first.fraunhofer.de> wrote:
>
>>  Hello,
>>
>> I studied the most recent ACSL 1.4 Manual. But I still don't know how to
>> program with it.
>> I would appreciate a working implementation of the "nbocc()" function.
>>
>> By the way I would like to know when to expect a patch, to repair the
>> problem with loop verification.
>>
>>
>> Thanks in advance
>>
>> Christoph
>>
>> _______________________________________________
>> Frama-c-discuss mailing list
>> Frama-c-discuss@lists.gforge.inria.fr
>> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>>
>>
>
>
> --
> Yannick
>
>

-- 
Yannick
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081103/533d9a47/attachment.htm