[Why3-club] creating an array of arrays

Yannick Moy moy at adacore.com
Wed Sep 19 18:39:15 CEST 2012

On 09/19/2012 06:13 PM, Johannes Kanig wrote:
> On 09/19/2012 06:09 PM, Alan Schmitt wrote:
>> 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.

Or use maps of maps, that would work indeed because map is not a mutable 
Yannick Moy, Senior Software Engineer, AdaCore

More information about the Why3-club mailing list