[Why3-club] creating an array of arrays

Johannes Kanig kanig at adacore.com
Wed Sep 19 18:13:29 CEST 2012

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.

Johannes Kanig <kanig at adacore.com>

More information about the Why3-club mailing list