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. declarative programming

  • Subject: [Frama-c-discuss] recursive programming vs. declarative programming
  • From: Christoph.Weber at first.fraunhofer.de (Christoph Weber)
  • Date: Mon Nov 10 09:31:28 2008
Salut,

today I wonder about the principles of recursive/ axiomatic programming and the things that I could do.

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.
To prove this, I thought about several things, that must be defined.

1. dest must be  a permutation of src, therefore my custom-made predicate: 

/*@ axiomatic IS_permutation {
logic integer is_permutation{L1,L2}(int* t1, int* t2, integer n); 
axiom is_permutation_occ{L1,L2}:
\forall int *t1, *t2, n, integer i; i < n ==>
nb_occ{L1}(t1,0,n-1,\at(t1[i],L1)) == nb_occ{L2}(t2,0,n-1,\at(t2[i],L2));
}
*/
(Problems are known)

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;
*/

all_permutations has to create permutations of a in dependency of x.

My idea was to implement a recursive function in C, which can do this and derive a possible implementation in ACSL.

C-code:
void all_permutation(int* a, int length, int n, int* number_of_perm)
{
    int temp;
    if (n == 0)
    { 
        *number_of_perm -= 1;
    }
    if(*number_of_perm == 0){
        return;
    }
    else
    { 
        for (int k=0; k <= n && *number_of_perm > 0 ; k++)
        { 
            // Swap a[k] und a[n]
            temp=a[n];
            a[n]=a[k];
            a[k]=temp;
            all_permutation(a, length, n-1, number_of_perm);
            // Swap-back a[k] and a[n] 
            temp=a[n];
            a[n]=a[k];
            a[k]=temp;
       } 
    }
}

ACSL:

/*@ 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.


Cheers

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