[Why3-club] Strange type error message on a ref array
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