--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on November 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