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

Andrei Paskevich andrei at lri.fr
Wed Nov 28 18:37:09 CET 2012


On 28 November 2012 15:52, Johannes Kanig <kanig at adacore.com> wrote:
> In Why3, you are not allowed to store mutable objects in other mutable
> objects.

Since Why3 v0.80, you are. In particular, one can store an array in a
reference, or, generally, in a mutable field of any record. What is
not allowed, is storing mutable values in recursive data structures
(such as lists) and in data structures defined via an abstract type.
For instance, one cannot define an array of references, because arrays
use maps (an abstract type) to store elements. The reason for this
restriction is that WP generator wouldn't know how to produce a new
value for the map after a modification in a stored reference.

> Here, you are storing a mutable array in a reference.

Which is okay. The problem with David's example is elsewhere and I'll
explain it in a next message.


More information about the Why3-club mailing list