--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on November 2008 ---
Hallo, 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. 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. 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. 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. > /*@ 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/. Cheers, -- Yannick -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081111/8616487d/attachment.htm