--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on November 2008 ---
Hi, The kind of properties you target, involving only linear arithmetic and data type axiomatizations, are certainly within the range of Frama-C with the Jessie plugin and ATP. At worst, you can always direct automatic proof by adding many intermediate logical assertions. But before you can test the tool, you need a consistent axiomatization of your ADT, which is the tough thing to do! Yannick On Tue, Nov 11, 2008 at 9:17 AM, Christoph Weber < Christoph.Weber@first.fraunhofer.de> wrote: > Salut, > > I just want to put the tool to a test. I need to know what can be done and > what is impossible. I realize that something like next_permutation is very > tough to prove. > > > > 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. > > Of course, but to prove that the result is correct, for example in this > permutation, I have to implement it twice, otherwise the correctness is just > an assumption. > > 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. > > I think that the result is very useful, otherwise i would not have to > annotate. And so far I had to reimplement every function. That is what a > complete specification is all about. > > 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. > > Yes, this will never work, it is just a sketch, I just wanted to draw my > thoughts, sorry for the confusion. > > > 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. > > This ordering-relation would be a lexicographic compare, that I do have. > > >> /*@ 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/. > > I see. > And there is no possibility to prove something like this (dont mind the > syntax)? > */*@* > 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; > */ > > > Cheers > > Christoph > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss@lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > > -- Yannick -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081111/13d80dfb/attachment.htm