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

Andrei Paskevich andrei at lri.fr
Thu Nov 29 11:19:22 CET 2012

On 29 November 2012 10:33, David MENTRE <dmentre at linux-france.org> wrote:
>> The pure snapshot types and the pure symbols defined on them do have
>> their use - not in programs, but in specifications (where every
>> mutable object is presented as a snapshot value).
> I must admit I am still not at ease with this dichotomy between
> immutable specification and mutable programs. In my specific case, I
> want to formalize a specification (i.e. without details about
> implementation) but with mutable states. For example, my specification
> states that "such state of the system should be updated under given
> condition". When formalizing it in Why3, I now understand that I
> should use Why3's program val definitions.

Yes, that's right.

>> I'd suggest to define "update" as a program function:
>>>  val update : unit -> t
> OK, I understand. However it does not work, with a syntax error on the arrow.

My bad, I used the old syntax :)

> 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 ()".

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.


More information about the Why3-club mailing list