[Checkers] Polymorphic Methods

[Michael Ernst]

Mahmood-

I think the below is OK.  It's a good thing to document, though.  I don't
think it's worth documenting in the manual, but maybe somewhere else.
(Or just cite the date and title of your email to the checkers list.)

                    -Mike


> From: Mahmood Ali <mahmood at MIT.EDU>
> To: checkers at lists.csail.mit.edu
> Subject: [Checkers] Polymorphic Methods
> Date: Tue, 24 Jun 2008 10:22:43 -0400
> 
> Greetings,
> 
> Flowing our discussions of polymorphic qualifiers, I wanted to point  
> out that my proposal is overly conservative in one case.  The proposal  
> (proposal 1) was that the polymorphic qualifier become being part of  
> qualifier hierarchy as supertype of all bottoms and subtype of all  
> supers, for the purposes of checking polymorphic methods.  The  
> alternative (proposal 2) would be creating N methods (with resolving  
> the polymorphic qualifier too all possible qualifiers) and type  
> checking them.
> 
> It fails to see a connection between the parameters and other non- 
> bottom values the user introduces.  Consider the following case:
> 
>     @PolyNull String identity(@PolyNull String s, @Nullable String m) {
>         return s;
>     }
> 
> The previous method type checks.  However the following two cases  
> don't type check
> 
>     // case 1
>     @PolyNull String identity(@PolyNull String s, @Nullable String m) {
>         if (s == null)
>             return null;  // doesn't type check, since null is not a  
> bottom qualifier
>         return s;
>     }
> 
>     // case 2
>     @PolyNull String weirdMethod(@PolyNull String s, @Nullable String  
> m) {
>         if (s == null)
>             return m;
>         return s;
>      }
> 
> Both of these methods type-check under the proposal 2 but not in  
> proposal 1.
> 
> In my opinion, this is still consistent with Java Generics.  And they  
> are not quite different from
> 
>     // analogues to case 1
>     <T> T weirdIdentity(T t) {
>         if (t instanceof String) // notice that String is a final class
>             return "m";
>         return t;
>     }
> 
>     // analogues to case 2
>     <T, E extends T> T wirdIdentity(E e, Date m) {
>         if (t instanceof Date)  // Date isn't final
>             return m;
>         return e;
>     }
> 
> Needless to say, both of the cases could still work if programmer  
> casts the return type to (@PolyNull String).
> 
> - Mahmood
> 
> 
> _______________________________________________
> checkers mailing list
> checkers at lists.csail.mit.edu
> https://lists.csail.mit.edu/mailman/listinfo/checkers