Frama-C-discuss mailing list archives

yannick.moy at gmail.com (Yannick Moy) · Tue Nov 4 11:20:42 2008

Hi,

All seems ok with the NbOcc axiomatic, I am going to explain it better so.

this seems to be a disguised recursion, covering any possibe case and could
> be written as:
>

yes, as I explained in a previous mail, axiomatization is a way to encode
recursive functions.

I am used to this kind of programming, were return values can be seen as
> such. My problem with the axiomatic is, to "trigger a return" meaning is the
> equality operator causing an asignment?
>

This is the difference between an operational semantics you get with
recursive operators and an axiomatic semantics you get with axioms. It
requires a mind-shift.

> By the way, continuing this thoughts, it seems to me as if in the
> underlined parts, there is no distinction between the current i and the i
> pointing to the next element. Shouldn't it be like this?
> *nb_occ(t,i,j,e) == nb_occ(t,i+1,j-1,e) + 1;*
> *nb_occ(t,i,j,e) == nb_occ(t,i+1,j-1,e);*
>
>
our axioms go the opposite way. They decrease [j] rather than increasing
[i], which is what is needed for the proof to be easily automated, since
loops usually iter on increasing indices. Try the example I sent to
understand it better. To prove the preservation of the loop invariant, we
get that
[c == nb_occ(a,0,i-1,d)].
Then, we must prove that at the end of loop, we have
[c' == nb_occ(a,0,i',d)],
with i' = i+1 and c' the new values of i and c.
It is possible to prove this automatically only if you get axioms that vary
the right bound of the range, which we did. Of course, you can perfectly add
axioms that vary the left part of the range, but be careful about not
changing the other bound like you do in the modified axiom you wrote.

HTH,

Yannick

> Well then,
>
> hope for help
>
>
> Christoph
>
> ----- Original Message -----
> *From:* Yannick Moy <yannick.moy@gmail.com>
> *To:* Christoph Weber <u20869@hs-harz.de>
> *Sent:* Monday, November 03, 2008 5:38 PM
> *Subject:* Re: [Frama-c-discuss] Axiomatic Definitions
>
> Hi,
>
> In fact, a definition could always be done through axiomatization. An axiom
> is a true fact for every x, y, etc that it universally quantifies, that
> relates the value of the function over these parameters to some other
> function applications, or some relations between x, y and z. You do not have
> to define a logic function to give it a meaning. E.g. here is an
> axiomatization of the nth decimal of pi:
>
> /*@ axiomatic Pi {
>   @   logic integer nth_of_pi(integer n);
>   @   axiom range:
>   @     \forall integer n; 0 <= nth_of_pi(n) <= 9;
>   @   axiom infinite:
>   @     \forall integer k, i;
>   @        0 <= i <= 9 ==> \exists integer n; k <= n && nth_of_pi(n) == i;
>   @ }
>   @*/
>
> Although I do not say much about nth_of_pi, I only state true facts about
> it, that are consistent with its meaning as the nth decimal of pi. Then,
> depending on the kind of programs you want to prove, you may end up adding
> more axioms to this list.
>
> It would be even better to provide inductive definitions that are provably
> well-defined, but we are not up to this yet!
>
> Please let me know if you have problems expressing you properties this way.
>
> Yannick
>
>
> On Mon, Nov 3, 2008 at 5:13 PM, Christoph Weber <u20869@hs-harz.de> wrote:
>
>>  Hi, I cannot post this on the list because I am currently outside the
>> institute therefore I cannot use the mail system. And have to rely on
>> another account
>>
>> My problem with axiomatized logic functions and predicates is, that I
>> don't understand, how the declaration of a predicate (e.g. nbocc()) is
>> backed up by the axioms. And why the predicate returns the count of
>> occurrences, in spite the fact, that nothing is expressed about execution.
>>
>> With the intermediate loop I meant the Why code.
>>
>> With a  recursive implementation, I see what the predicate does and how it
>> is done. In the axiomatic case I see it not.
>> If I have (at least partially) understood why it does what, I will create
>> something on my own. Until then I wait for wisdom to reveals itself :)
>>
>> 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 4:36 PM
>> *Subject:* Re: [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
>>
>> ------------------------------
>>
>> _______________________________________________
>> 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
>
>
> _______________________________________________
> 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/20081104/3b2e60f4/attachment-0001.html