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] recursive programming vs. declarativeprogramming

Salut,

I just want to put the tool to a test. I need to know what can be done and what is impossible. I realize that something like next_permutation is very tough to prove.


  You must realize it is in general hard to duplicate in the logic all the details of implementation, and it is not generally useful to do this. 

  Of course, but to prove that the result is correct, for example in this permutation, I have to implement it twice, otherwise the correctness is just an assumption.

  Logical annotations should be here to help proving some useful property about the program, not to duplicate the same amount of information as found in the program. 

  I think that the result is very useful, otherwise i would not have to annotate. And so far I had to reimplement every function. That is what a complete specification is all about.

  It is all the more important to realize this if you want to work with automatic provers, that cannot handle complex VC automatically.



    My goal is to define a function called "next_permutation(int* src, int* dest)". In essence, it returns the next greater permutation. Multiple appearances of the same element are allowed.

    2. dest must be the next greater permutation src,  therefore, it must be proven, that no permutation exists, which is > src and < dest.
    /*@
    next_permutation (int* a, int* b)=
    is_permutation(a,b)==>a>b &&
    \forall x all_permutations(a,x)>a ||
    \forall x all_permutations(a,x)<b;
    */

  Beware that your order on [a] and [b] here is the ordering of C pointers??? There must be a problem here. 

  Yes, this will never work, it is just a sketch, I just wanted to draw my thoughts, sorry for the confusion.


  Plus you compare in the following lines sets and elements, which is not typable. Again, it is up to you to define an ordering relation between permutations.

  This ordering-relation would be a lexicographic compare, that I do have.

    
    /*@ axiomatic ALL_permutation {
    @ 
    @ logic ??? all_permutation{L}(int* a, integer length, integer n, int* number_of_perm); 

    @ axiom nth_permutation{L}:
            \forall int *a, *number_of_perm, integer length, n; *number_of_perm == 0 ==> ???return??? ;
    @ axiom next_permutation{L}:
            \forall int *a, *number_of_perm, integer length, n; n == 0 ==> *number_of_perm -= 1;
    @ axiom recursive_call{L}:
            \forall int *a, *number_of_perm, integer length, n, k, j; 0 <= k < n && n != 0 && *number_of_perm != 0 ==> 
            swap(a+n, a+k) ==>
            all_permutation(a, length, n-1, number_of_perm) ==>
           swap(a+n, a+k);
    @ }
    @*/

    You see the problem, this mix of functional and declarative programming is difficult.

    I would like a suggestion how this could be solved or if there will be a solution in the near future.

  No, there is no possible solution in this sense. Reasoning about sets and ADT in general is complex, and many research is done on this subject. ACSL is not going to "solve" this problem. I suggest that you look at examples of proved programs, like those found in http://why.lri.fr/examples/.

  I see. 
  And there is no possibility to prove something like this (dont mind the syntax)?
  /*@
  next_permutation (int* a, int* b)=
  is_permutation(a,b)==>a>b &&
  \forall x all_permutations(a,x)>a ||
  \forall x all_permutations(a,x)<b;
  */


  Cheers

  Christoph
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081111/4cbe5d4c/attachment.html