Created by @alexanderjsummers on 2018-06-04 15:42
Last updated on 2018-06-05 21:05
Quantified permissions are currently encoded in such a way that the mapping between the instances of the quantified variable and the corresponding set of field receivers is assumed to be a bijection, at least for the values of the quantified variable for which permission is required. This leads indirectly to the assumption that, when ranging over the whole of a particular type, the type has the same size as Ref. This is incorrect. For example:
#!scala
field val : Int
function bool2Ref(b: Bool) : Ref
ensures result != null
//ensures bool2Ref(true) != bool2Ref(false) // injectivity - doesn't change the behaviour
method m(x:Ref)
requires forall b:Bool :: acc(bool2Ref(b).val)
{
x.val := 42
//:: MissingOutput(assert.failed:assertion.false, /carbon/issue/239)
assert false
}
Quantified permissions are currently encoded in such a way that the mapping between the instances of the quantified variable and the corresponding set of field receivers is assumed to be a bijection, at least for the values of the quantified variable for which permission is required. This leads indirectly to the assumption that, when ranging over the whole of a particular type, the type has the same size as
Ref. This is incorrect. For example: