Frama-C-discuss mailing list archives

yannick.moy at gmail.com (Yannick Moy) · Tue Nov 11 11:49:24 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

Frama-C-discuss mailing list archives

[Frama-c-discuss] recursive programming vs. declarativeprogramming