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

Hello and thank you for the quick response,
I see "axiomatic" is the way to do it.
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.
Is there a relation between axiom-names and evaluation?
Where is it expressed, that an array has to be processed?
Is there a tutorial which would help to understand this problem?
Is there something intermediate that contains a loop?

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081103/b48d37fb/attachment.html