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

David MENTRE dmentre at linux-france.org
Thu Nov 29 11:59:46 CET 2012

Hello Andrei,

2012/11/29 Andrei Paskevich <andrei at lri.fr>:
> My bad, I used the old syntax :)

In fact, I overlooked table A.1 which is clear about the syntax to use.

>> Using "val update () : t" works but then I get another error message
>> on c: "This expression prohibits further usage of variable c". I am
>> still missing something. :-)
>> """
>> module Test2
>>   use import ref.Ref
>>   use import array.Array
>>   type t = array int
>>   val c : ref t
>>   val update () : t
>>   let do_update () : () =
>>    c := update ()
>> end
>> """
> This is, again, related to the fact that WhyML program types contain
> information about memory locations. Let's see. On one hand, the type
> of "update" says that this function produces a new array out of
> nowhere on every call. The system concludes that this array must be
> fresh, that is, a new memory cell must be allocated at every call. On
> the other hand, the type of ":=" is "ref 'a -> 'a -> unit", that is,
> the type of the new value must be exactly the same as the type of the
> reference contents, _including_ the memory annotations. So, when you
> write "c := update ()", the type of the result of "update ()" is
> unified with the type of "c.contents". But this contradicts the
> freshness of the former type : since the new array is fresh, no
> existing variable can mention that memory cell in its type. And so
> WhyML tells you that cannot use "c" after calling "update ()".

Thank you for your clear explanation!

> To replace a mutable object stored in a reference with another mutable
> object, occupying different memory cells, you have to use the
> primitive assignment operation:
>> c.contents <- update ()
> In this case, WhyML does not unify memory locations, only the types proper.

Ok, that's clear and it works on my model. :-)

>From a strict user point of view, the difference between "c :=" and
"c.contents <-" is thin and a bit confusing, even if I now understand
the underlying logic. Until now, I thought ".contents" field of a
reference was some Why3 internal and that the user should not worry
about it. ;-)

As memory location are so important, maybe they should appear in some
way in type annotation and error messages. I don't have any concrete
syntax to propose, though.

Once again, many thanks for the detailed explanation,
Best regards,

More information about the Why3-club mailing list