Frama-C-discuss mailing list archives

Christoph.Weber at first.fraunhofer.de (Christoph Weber) · Tue Nov 4 11:05:54 2008

Hi,

I have reviewed the the NBocc example:

/*@ axiomatic NbOcc {
@ // nb_occ(t,i,j,e) gives the number of occurrences of e in t[i..j]
@ // (in a given memory state labelled L)

@ logic integer nb_occ{L}(double t[], integer i, integer j, @ double e); 

@ axiom nb_occ_empty{L}:    \forall double t[], e, integer i, j; i > j ==> nb_occ(t,i,j,e) == 0;
@ axiom nb_occ_true{L}:         \forall double t[], e, integer i, j; i <= j && t[j] == e ==>  nb_occ(t,i,j,e) == nb_occ(t,i,j-1,e) + 1;
@ axiom nb_occ_false{L}:       \forall double t[], e, integer i, j; i <= j && t[j] != e ==> nb_occ(t,i,j,e) == nb_occ(t,i,j-1,e);

@ }
@*/

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

logic integer occ_value(int* a, int index, int length, int value) =
(index == length) ? 0 : ( 
(a[index] == value) ? 1 + list_length(a, index+1, length, value) :
list_length(a, index+1, length, value)) ;

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?

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);

Well then,

hope for help

Christoph
  ----- Original Message ----- 
  From: Yannick Moy 
  To: Christoph Weber 
  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 
      To: Christoph Weber 
      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 
          To: Christoph Weber 
          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 
              To: Christoph Weber 
              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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081104/0fae6fe2/attachment.htm