# [Why3-club] permut fix

Jean-Christophe Filliâtre Jean-Christophe.Filliatre at lri.fr
Tue Mar 11 08:56:05 CET 2014

```Dear Jean-Jacques,

Le 11/03/2014 07:33, Jean-Jacques Levy a écrit :
> following problem of early February, is there a fix for a consistent theory of permutations on arrays ?

Yes, we have fixed this issue two weeks ago (I thought I had replied to
this list, my mistake).

We did the following:

- In both maps and arrays, permutation predicates are no more defined
inductively, but rather using theory map.Occ that defines the number of
occurrences of value v in a[l..u[ (i.e. permutation now means that, for
any value v, its number of occurrences in the two sub-arrays coincide).

- Library array.ArrayPermut exports the following predicates:

- permut a1 a2 l u : a1[l..u[ is a permutation of a2[l..u[
and values outside interval [l..u[ are ignored
(and arrays have the same length, and interval [l..u[ is legal)

- permut_sub a1 a2 l u : a1[l..u[ is a permutation of a2[l..u[
and values outsides interval [l..u[ are identical
(and arrays have the same length, and interval [l..u[ is legal)

- permut_all a1 a2 : array a1 is a permutation of array a2

- We have proved the consistency of these libraries (map.Occ,
map.MapPermut and array.ArrayPermut) using Coq. (These Coq proofs are
shipped with Why3 and replayed every night as part of our regression tests.)

- We have updated all the examples in our gallery. In the process, we
have even improved the level of proof automation. See for instance
examples/quicksort.mlw, which is now fully automated (and even has a
nicer specification).

Best regards,
--
Jean-Christophe

```