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

Andrei Paskevich andrei at lri.fr
Wed Nov 28 23:38:54 CET 2012


On 28 November 2012 15:25, David MENTRE <dmentre at linux-france.org> wrote:
> Hello,
>
> Using Why3 0.80, I can write this kind of code:
> """
> module Test
>   use import ref.Ref
>
>   val c : ref int
>   function update : int
>
>   let do_update () : () =
>    c := update
> end
> """
>
> However, when I apply this pattern to a data structure with an array,
> it fails with a type error message I don't understand:
> """
> module Test2
>   use import ref.Ref
>   use import array.Array
>
>   type t = array int
>   val c : ref t
>   function update : t
>
>   let do_update () : () =
>    c := update
> end
> """
>
> """
> $ PATH=/usr/local/stow/why3-0.80/bin/:/usr/local/bin why3 -C why3.conf
> -I . test.mlw
> File "test.mlw", line 20, characters 3-4:
> This expression has type ref <rho:array <rho1:map int int> int> (array
> <rho1:map int int> int), but is expected to have type ref <rho2:array int>
> (array int)
> """
>
> Could somebody explain to me what I am doing wrong?

First of all, pure logical symbols (functions, predicates, constants)
cannot work with mutable datatypes, only with their pure "snapshots".
When you define a pure symbol such as "update" with a mutable type in
the result, this is accepted, but the returned value will have a pure
logical type (an immutable record containing a map and an integer
length) which is not unifiable with the real mutable type of the
contents of "c". So, the error message tells you "type mismatch: you a
trying to assign a pure snapshot type `array int' to a reference
holding a mutable program type `array <...> int'" [*].

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 think we must
simply forbid using symbols like "update" in program expressions, with
a comprehensible error message.

I'd suggest to define "update" as a program function:
>  val update : unit -> t

Best,
Andrei

[*] In Why3, the memory locations occupied by any mutable object are
computed statically and stored in the object's type. Thus, when you
define a global reference "c", the actual type of "c" is not simply
"ref (array int)", but "ref <rho:array <rho1:map int int> int> (array
<rho1:map int int> int)", where "rho1" is a mutable memory cell
occupied by the array (this cell contains an immutable map) and "rho2"
is a mutable memory cell occupied by the reference "c" (this cell
contains the array). The both cells "rho" and "rho1" are reserved at
the declaration of "c".



More information about the Why3-club mailing list