Cloning part of mutable structure
Similar attempt than in #51, but here the question is more what would be the right way to use.
The important points to try to keep are:
- the field minimum is not mutable
- there is an invariant
module T
use int.Int
type t_mutable = mutable { }
type t = {
ghost minimum: int;
t_mutable: t_mutable;
}
val create (ghost i:int) : t
ensures { result.minimum = i }
val set (x:t) (i:int) : unit
requires { x.minimum <= i }
writes { x.t_mutable }
exception Unset
val get (x:t) (i:int) : int
ensures { x.minimum <= result }
raises { Unset -> true }
end
module T2
use int.Int
type t_mutable = {
mutable v: int;
mutable set': bool;
}
type t = {
ghost minimum: int;
t_mutable : t_mutable;
}
invariant { t_mutable.set' -> minimum <= t_mutable.v }
let set (x:t) (i:int) : unit
requires { x.minimum <= i }
=
x.t_mutable.v <- i;
x.t_mutable.set' <- true
let create (ghost i:int) : t
ensures { result.minimum = i } =
{ minimum = i;
t_mutable = { set' = false; v = 0 }
}
exception Unset
let get (x:t) (i:int) : int
ensures { x.minimum <= result }
raises { Unset -> true }
=
if not x.t_mutable.set' then raise Unset;
x.t_mutable.v
clone T with
type t_mutable = t_mutable,
val create = create,
val set = set,
exception Unset = Unset,
val get = get
end
Currently the message is that the two t types are not the same. The substitution of type t = t
, can't be currently added in the clone stanza because t is defined in T.