[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?

Yes.

> 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,
david



More information about the Why3-club mailing list