• Andrei Paskevich's avatar
    examples/vstte10_queens: strong updates · 340ffc11
    Andrei Paskevich authored
    1. Strong region updates can only work with direct assignments, e.g.
         r.contents <- something_completely_different
       but not with functions such as (:=) : ref 'a -> 'a -> unit
       Why3 requires 'a to be instantiated with one concrete type,
       not with a bunch of types that differ in their regions.
    2. Strong region updates will restrict the updated regions to their
       covers. However, in the current implementation, Why3 does not know
       if the region corresponding to the field "contents" is the only
       cover for 'a in the type [ref 'a] or if there is a way to retrieve
       'a from [ref 'a] without going through "contents". Therefore, to
       ensure soundness, a strong update of r.contents will forbid to
       use r itself. A solution consists in writing an adhoc "reference"
       type, where the mutable contents (O.t in this case) is explicitly
       given in the type definition. Then the strong update of the field
       containing O.t will preserve the covering "reference".
       This problem is fixed in the "new system", where mutable types
       carry information about the access paths of the type variables.
       There, "r.contents <- something_different" preserves r.