[Why3-club] permut fix

Jean-Jacques Levy jean-jacques.levy at inria.fr
Tue Mar 11 09:42:15 CET 2014


Many thanks. So your advice is to use the development version. -JJ-

Le 11 mars 2014 à 15:56, Jean-Christophe Filliâtre <Jean-Christophe.Filliatre at lri.fr> a écrit :

> 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
> 
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club




More information about the Why3-club mailing list