--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on November 2008 ---
> Yet my problem remains, I could not easily do it on my own, unless I know > why and how it does what I intend to do. > Except from the missing reads clause that is now inferred, the new axiomatic is similar to what was done previously for axiomatized logic functions and predicates: you declare function or predicate, and you define them through axioms. > Is there a relation between axiom-names and evaluation? > Axioms are just true formulas given to automatic provers to use in any way they like. Or in proof assistants, but then you must tell how to instanciate them. > Where is it expressed, that an array has to be processed? > Axioms are expressed in a way that is suitable to facilitate the proof, but they do not express anything about execution. > Is there a tutorial which would help to understand this problem? > Nothing more than what I explained ... > Is there something intermediate that contains a loop? > like an example ? the example I sent contained a loop. Do you mean something else? Perhaps you could try on your example and tell us what is missing in your case? I'm sure we can make it in some finite time! ;0) Yannick > HFH, > 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 3:17 PM > *Subject:* Re: [Frama-c-discuss] Axiomatic Definitions > > 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 > > > _______________________________________________ > 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 -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081103/381ac98d/attachment.htm