[Checkers] Flow and IGJ

[Michael Ernst]

Mahmood-

> When porting it to IGJ, I have the following case:
>    @ReadOnly Date d = new @Mutable Date();
>    d.setDate(3);  // d guaranteed to be mutable
> 
> I find it to be a bit troubling from readability standpoint and (I  
> assume) would complicate the mutation rules.

I don't think it complicates the mutation rules.  Those rules are written
without regard to flow-sensitive type refinement, and the type refinement
is best expressed as introduction of new temporary variables with the more
accurate types (or replacement of the old type for a declaration).

The readability feels more important to me.  In each case you can perform
additional operations that you couldn't before, but all of the guarantees
you had about the object do continue to hold (but those guarantees are
essentially vacuous, when the declared qualifier is the top of the type
system).

Is the problem the name "@ReadOnly", which suggests that the thing doesn't
change?  We do know that it's allowed to change out from under the
reference d -- it's just that in this case it changes via d itself!

> I think that flow  
> should only operate if the user doesn't specify a qualifier.

That restriction would be OK with me -- at least, making it the default
would be OK, and maybe it should be overridable.

> What should be the default for flow: only propagate if user doesn't  
> specify qualifiers, or always propagate if the value of the variable  
> is guaranteed to be a subtype of variable declaration qualifier?

Either default is OK with me.

                    -Mike