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

David MENTRE dmentre at linux-france.org
Wed Nov 28 17:08:26 CET 2012

2012/11/28 Johannes Kanig <kanig at adacore.com>:
> I don't understand what would be the difference between array.mlw and
> staticarray.mlw? Do your "static" arrays have a static length?


> Static as
> in "known at compile time", not as in "cannot be changed for a given array".

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

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.

Thank you for the feedback,

More information about the Why3-club mailing list