[Why3-club] creating an array of arrays
alan.schmitt at polytechnique.org
Wed Sep 19 21:44:27 CEST 2012
Jean-Christophe Filliâtre <Jean-Christophe.Filliatre at lri.fr> writes:
>>> The solution for your specific problem would be indeed to define your
>>> own Matrix module. It is easy enough to do.
> This is indeed the right answer. We have to apologize for the current
> state of the manual regarding WhyML, which should state this
> limitation clearly.
>> Or use maps of maps, that would work indeed because map is not a mutable
> A map of maps is a purely applicative data structure (it belongs to
> the logic world). Using it in programs is fine. The alternative above
> suggested by Johannes is to use it as the *model* of some matrix data
> structure (so that the program is manipulating values of some abstract
> data type, not maps of maps).
I'm going to try to provide the students with a simple Matrix module,
probably based on a map from int * int to int. The goal here is to teach
them simple program invariants.
Thanks for all the suggestions.
More information about the Why3-club