--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on May 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] ACSL-1.9, Example 2.46



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