[Why3-club] Strange type error message on a ref array

David MENTRE dmentre at linux-france.org
Wed Nov 28 16:31:06 CET 2012

2012/11/28 Johannes Kanig <kanig at adacore.com>:
> Sounds good, but note that the type array is already basically a
> reference to a map. The only difference is that the type array also
> comes with the length of the array, and index validity preconditions for
> the access/update.

Yes, I saw that.

> So if you don't need the length stuff, then "ref + map" is good,
> otherwise you can also use "array" directly.

(sigh) Except that in my model (1) I want to do the ref stuff (i.e.
assign a new value for the whole array) and (2) I need the length of
the array (that's why I used an array in the first place instead of a

One solution would be to copy/paste array.mlw into staticarray.mlw and
adapt it to my needs. I need to think about it (because I hate not
reusing existing std library).

Best regards,

More information about the Why3-club mailing list