[Why3-club] creating an array of arrays

Jean-Christophe Filliâtre Jean-Christophe.Filliatre at lri.fr
Wed Sep 19 20:14:16 CEST 2012

>>> My question is twofold: is it possible to do this using arrays? If not,
>>> what is the alternative? Creating a matrix module similar to the array
>>> module? Or maybe directly use maps?
>> It's not possible AFAIK. The reason is that you cannot nest mutable
>> structures (you would otherwise potentially create aliasing). Also, you
>> cannot put records with mutable fields into an array, for the same
>> reason.
>> 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 

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


More information about the Why3-club mailing list