[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).

The relevant commit is ca0ec4aab2115c (see also 355efcc626b3605).
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



More information about the Why3-club mailing list