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