On Fri, 16 Feb 2018, Claude Marché wrote:
>
> I suggest to look at
>
> http://toccata.lri.fr/gallery/sorting.en.html
>
> and in particular to
>
> http://toccata.lri.fr/gallery/mergesort_list.en.html
>
> that provides a verified implementation of OCaml's List.sort
>
> There is a difference though: since the given 'compare' function should
> be required to defined a proper order relation, the code is written
> under a form similar to a functor.
>
> This code is not part of Why3's standard library, as far as I know.
Thanks for the pointers!
julia
>
> - Claude
>
> Le 16/02/2018 à 11:11, Julia Lawall a écrit :
> > Hello,
> >
> > Does why3 offer sorted lists. Concretely, is it possible to write
> > something like List.sort compare l in OCaml? I saw the sorted theories in
> > the List documentation, but I see only lemmas, no functions. Is it
> > necessary to implement sorting explicitly?
> >
> > thanks,
> > julia
> > _______________________________________________
> > Why3-club mailing list
> > Why3-club@lists.gforge.inria.fr
> > https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> >
>
> --
> Claude Marché | tel: +33 1 69 15 66 08
> INRIA Saclay - Île-de-France |
> Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/
> F-91405 ORSAY Cedex |
> _______________________________________________
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
