# 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*: yannick.moy at gmail.com (Yannick Moy)*Date*: Tue Nov 11 02:52:57 2008*In-reply-to*: <1E09044D1CD240E984A45571FC80DD96@AHARDPLACE>*References*: <1E09044D1CD240E984A45571FC80DD96@AHARDPLACE>

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

**Follow-Ups**:**[Frama-c-discuss] recursive programming vs. declarativeprogramming***From:*Christoph.Weber at first.fraunhofer.de (Christoph Weber)

**References**:**[Frama-c-discuss] recursive programming vs. declarative programming***From:*Christoph.Weber at first.fraunhofer.de (Christoph Weber)

- Prev by Date:
**[Frama-c-discuss] Composition of COMPLEX Contracts** - Next by Date:
**[Frama-c-discuss] Composition of COMPLEX Contracts** - Previous by thread:
**[Frama-c-discuss] recursive programming vs. declarative programming** - Next by thread:
**[Frama-c-discuss] recursive programming vs. declarativeprogramming** - Index(es):