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

David MENTRE dmentre at linux-france.org
Thu Nov 29 10:33:31 CET 2012


Hello Andrei,

2012/11/28 Andrei Paskevich <andrei at lri.fr>:
> 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".

OK, I understand. Thank you for the explanations.

> 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.


> 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.

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
"""

Best regards,
david



More information about the Why3-club mailing list