Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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