Hi Benoit,
The problem here is that Why3 accepted a clone instruction which was,
strictly speaking, invalid, and gave it a meaning which made it valid, but
which was not the one you wanted. Here is what happened:
1. The type 'storage' declared in Afunction is immutable, because WhyML
operates under assumption "no hidden effects, no hidden state", and thus
everything is immutable unless explicitly declared otherwise. Any module
that uses Afunction (as an interface to a library) assumes that values of
type 'storage' do not change.
2. Module Test declares a mutable type 'storage' but then clones Afunction
and instantiates Afunction's immutable type 'storage' with this mutable
type. Why3 should have refused this instantiation but didn't [bug 1]. What
it did instead is it instantiated Afunction's immutable type 'storage' with
the _snapshot_ type '{storage}' (note the curly braces). Snapshot types
serve to represent momentary states of mutable values and as such they are
immutable.
3. As a consequence of this, the cloned function 'exec' now has type
'{storage} -> init'. This should have led to typing error at the function
'update': a mutable value cannot be passed directly to a function expecting
a snapshot, and thus the type of 's' was inferred to be '{storage}', which
should have conflicted with the type annotation 'storage' [bug 2]. The
code, however, was rejected, when it tried to write into 's', since 's',
internally, was considered immutable.
The correct way of doing what you wanted is to declare the type 'storage'
in Afunction as mutable : 'type storage = abstract mutable { }'. (By the
way, simply writing 'type storage' is equivalent to 'type storage =
abstract { }'.)
As for us, we have two bugs to fix:
bug 1: Immutable types shouldn't be allowed to be instantiated by mutable
types.
bug 2: Explicit type annotations without curly braces should not be
resolvable as snapshots.
Thanks for the report!
Best,
Andrei
On Mon, 29 Apr 2019 at 22:31, Benoit Rognier <benoit.rogn...@edukera.com>
wrote:
> Hello, Why3-club,
>
> The following code
>
> theory Afunction
> use int.Int
>
> type storage
>
> val function exec storage : int
>
> end
>
> theory Test
> use int.Int
> use Afunction
>
> type storage = {
> mutable a : int;
> }
>
> clone Afunction as Af with type storage = storage
>
> let update (s : storage) = s.a <- Af.exec s
>
> end
>
> generates the following compilation error :
>
> line 24, characters 1-17: This assignment modifies a value of the
> immutable type {storage}
>
> What does it mean ? and why is the type 'storage' considered to be
> immutable ?
> Thank you,
> Benoit Rognier
> _______________________________________________
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
