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

Johannes Kanig kanig at adacore.com
Wed Nov 28 17:16:10 CET 2012

On 11/28/2012 05:08 PM, David MENTRE wrote:
> Static as in "purely functional like map but with a length attribute".
> In other words, take array.mlw, remove the mutable attribute of "elts"
> and adapt "set" and the like accordingly. Maybe the name "static" is
> badly chosen. ;-)

Ah, I get it.

> As I said, I am trying to formally model a real system spec and it is
> important for me to be as close as possible to the spec. I have
> several options to make this model so maybe my Staticarray approach is
> not the right way to do it.

Well, I think the functional_array (would be a better name) approach is
the right one, but maybe other people have a better idea. Yes, it would
amount removing the "mutable" keyword from the array.mlw module and
change accordingly.

Johannes Kanig <kanig at adacore.com>

More information about the Why3-club mailing list