--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on November 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