--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on November 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Axiomatic Definitions



> 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