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 test

  • Subject: [Frama-c-discuss] axiomatic permut test
  • From: Christoph.Weber at first.fraunhofer.de (Christoph Weber)
  • Date: Fri Nov 7 09:21:55 2008
Hi,

to get a better understanding of the axiomatic stuff I implemented "axiomatic Permut".

/*@ axiomatic Permut {
// permut{L1,L2}(t1,t2,n) is true whenever t1[0..n-1] in state L1
// is a permutation of t2[0..n-1] in state L2

predicate permut{L1,L2}(int* t1, int* t2, integer n);

axiom permut_refl{L}:
\forall int *t, integer n; permut{L,L}(t,t,n);

axiom permut_sym{L1,L2} :
\forall int *t1, *t2, integer n; 
permut{L1,L2}(t1,t2,n) ==> permut{L2,L1}(t2,t1,n) ;

axiom permut_trans{L1,L2,L3} :
\forall int *t1, *t2, *t3, integer n;
permut{L1,L2}(t1,t2,n) && permut{L2,L3}(t2,t3,n) ==> permut{L1,L3}(t1,t3,n) ;

axiom permut_exchange{L1,L2} :
\forall int *t1, *t2, integer i, j, n;
\at(t1[i],L1) == \at(t2[j],L2) &&
\at(t1[j],L1) == \at(t2[i],L2) &&
(\forall integer k; 0 <= k < n && k != i && k != j ==>
\at(t1[k],L1) == \at(t2[k],L2)) ==> permut{L1,L2}(t1,t2,n);
}
*/
/*@
requires 0 <= length;
requires \valid_range(array1, 0, length-1);
ensures permut{Old,Here}(array1, array1, length);
*/
void permute_test(int* array1, int length){}


First, i changed the datatypes. Second i added a Lable axiom permut_refl{L}: because Jessie told me it was missing.

Now I wonder why something as simple as nothing cannot be proven. I hope the mistake is mine.

Cheers

Christoph
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081107/4ca5fca3/attachment.html