--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on November 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] recursive programming vs. declarative programming



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