--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on November 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] axiomatic permut redefined



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