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] axiomatic permut redefined

  • Subject: [Frama-c-discuss] axiomatic permut redefined
  • From: Christoph.Weber at first.fraunhofer.de (Christoph Weber)
  • Date: Fri Nov 7 10:04:51 2008
Hi again,

I have another problem I need help with.

While I don't understand the axiomatic's well enough to do some serious proving, I tried to implement a more functional approach of defining permut. The idea is to count the occurrence of every element in each array and to compare. Therefore I reused the NB_occ, given by Yannick:

/*@ axiomatic NbOcc {
@ // nb_occ(t,i,j,e) gives the number of occurrences of e in t[i..j]
@ // (in a given memory state labelled L)
@ logic integer nb_occ{L}(int* t, integer i, integer j, 
@ int e); 
@ axiom nb_occ_empty{L}:
@ \forall int *t, e, integer i, j;i > j ==> nb_occ(t,i,j,e) == 0;
@ axiom nb_occ_true{L}:
@ \forall int *t, e, integer i, j; i <= j && t[j] == e ==> nb_occ(t,i,j,e) == nb_occ(t,i,j-1,e) + 1;
@ axiom nb_occ_false{L}:
@ \forall int *t, e, integer i, j; i <= j && t[j] != e ==> nb_occ(t,i,j,e) == nb_occ(t,i,j-1,e);
@ }
@*/

/*@ axiomatic IS_permutation {
logic integer is_permutation{L1,L2}(int* t1, int* t2, integer n); 
axiom is_permutation_occ{L1,L2}:
\forall int *t1, *t2, n, integer i; i < n ==>
nb_occ{L1}(t1,0,n-1,\at(t1[i],L1)) == nb_occ{L2}(t2,0,n-1,\at(t2[i],L2));
}
*/


/*@
requires 0 <= length;
requires \valid_range(array1, 0, length-1);
ensures is_permutation{Old,Here}(array1, array1, length);
*/
void permute_test(int* array1, int length){}

Doing this, I get following message:

Uncaught exception: Failure("Unexpected internal region in logic")

Unfortunately I have no clue what this means.
I would appreciate a hint whether the idea is doable and where are my mistakes.

Cheers 
Christoph
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081107/1be48b25/attachment.htm