--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on May 2015 ---
A suggestion: For clarity, this example should have an axiom @ axiom permut_refl{L1,L2} : @ \forall double *t1, *t2, integer n; @ (\forall integer i; 0 <= k < n ==> \at(t1[k],L1) == \at(t2[k],L2)) ==> permut{L1,L2}(t1,t2,n) ; instead of the existing permut_refl. The above serves as a base case from which to do exchanges. The above is not absolutely necessary because one can prove it by a transitive combination of two swaps between the same i,j indices, but that hardly makes for a good pedagogical example. Similarly the existing permut_refl is not essential, as it can also be proved from exchange and trans, or from the new refl. - David