[Why3-club] creating an array of arrays

Alan Schmitt 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
>> structure.
> 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 mailing list