[Checkers] [Checker] Method Invocability

[Mahmood Ali]

Greetings Daniel,

Sorry if my comments are a bit irrelevant, as I joined the thread a  
bit late.

[Daniel said:]
> Is there a way to find out the name of the method
> and the (annotated) type of the object while checking method  
> invocation?
> I was planning to check the method's name and the object's state and
> then changing the object's state accordingly.
Yes, there is a way.  I assume that you are planning to do pattern  
matching to determine state change.  In particular, any open()/close()  
method invocation sets its receiver to Open/Close type.  Is this  
correct?

[Daniel said:]
> Or do I have to use a different approach here?
Yes.  There is another more general approach.  I will submit to you a  
proposal (and probably a prototype) soon.

[Daniel then Mike said:]

>> Well, I actually did not want to check that the arguments are  
>> compatible
>> but that it is legal to call the method.
> The method call is legal exactly if the arguments at the call site are
> compatible with the parameters in the method declaration.

Mike is indicating that it's legal to call a method iff two conditions  
hold (they are actually one condition broken to two):
1. Passed arguments are subtypes of their corresponding parameter  
types in the method declaration.  This is what Mike is suggesting.
2. The call site is of a type that allows to call the method given its  
receiver type, e.g. can call Mutable methods only on Mutable call sites.

It is seems that you are focusing on the second condition rather than  
the first condition.

- Mahmood