[Why3-club] creating an array of arrays

Alan Schmitt alan.schmitt at polytechnique.org
Thu Sep 20 16:07:08 CEST 2012


Johannes Kanig <kanig at adacore.com> writes:

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

Thank you for the suggestion. It will also be an interesting warm-up
exercise for the students.

Alan



More information about the Why3-club mailing list