org.jmlspecs.jml4.rac.runtime
Class JMLSurrogate

java.lang.Object
  org.jmlspecs.jml4.rac.runtime.JMLSurrogate

public abstract class JMLSurrogate
extends java.lang.Object

The common behavior of all surrogate classes. Each interface surrogate class, generated by jmlc, is supposed to be inherit behavior specified in this class.

Version:

$Revision: 1.11 $

Author:

Yoonsik Cheon

Field Summary

static java.util.Map<org.jmlspecs.jml4.rac.runtime.JMLSurrogate.MapKey,java.lang.reflect.Method>

methods The shared cache for dynamically looking up methods.

Method Summary

static java.lang.reflect.Method	getAccessor(java.lang.Class clazz, java.lang.String name) Returns the accessor (getter) method of a ghost field or a model field, name, declared in the type, clazz.
static java.lang.reflect.Method	getMethod(java.lang.Class clazz, java.lang.String name, java.lang.Class[] types) Returns a method object that reflects the specified public member method of the class or interface, clazz.
JMLCheckable	getSelf() Returns the delegee of this object.
static java.lang.reflect.Method	getSetter(java.lang.Class clazz, java.lang.String name, java.lang.Class type) Returns the setter method of the ghost field, name, of type type, declared in class, clazz.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

methods

public static final java.util.Map<org.jmlspecs.jml4.rac.runtime.JMLSurrogate.MapKey,java.lang.reflect.Method> methods

The shared cache for dynamically looking up methods. This map contains assertion check methods, accessor methods, and setter methods that are dynamically looked up for runtime assertion checking. The keys are instances of the class KeyMap.

 public invariant methods != null &&
   (\forall MapKey k; methods.containsKey(k); 
      methods.get(k) instanceof Method);
 

Method Detail

getSelf

public JMLCheckable getSelf()

Returns the delegee of this object. The delegee is the object that this surrogate object exists for.

getMethod

public static java.lang.reflect.Method getMethod(java.lang.Class clazz,
                                                 java.lang.String name,
                                                 java.lang.Class[] types)
                                          throws java.lang.NoSuchMethodException,
                                                 java.lang.SecurityException

Returns a method object that reflects the specified public member method of the class or interface, clazz. The name parameter is a string specifying the simple name of the desired method. The types parameter is an array of class objects that identify the method's formal parameter types, in declared order. If it is null, it is treated as if it were an empty array.

Throws:

java.lang.NoSuchMethodException

java.lang.SecurityException

getAccessor

public static java.lang.reflect.Method getAccessor(java.lang.Class clazz,
                                                   java.lang.String name)
                                            throws java.lang.NoSuchMethodException,
                                                   java.lang.SecurityException

Returns the accessor (getter) method of a ghost field or a model field, name, declared in the type, clazz. This method looks for the method first at the local cache, and then, if fails, the class object itself.

Throws:

java.lang.NoSuchMethodException

java.lang.SecurityException

getSetter

public static java.lang.reflect.Method getSetter(java.lang.Class clazz,
                                                 java.lang.String name,
                                                 java.lang.Class type)
                                          throws java.lang.NoSuchMethodException,
                                                 java.lang.SecurityException

Returns the setter method of the ghost field, name, of type type, declared in class, clazz. This method looks for the method first at the local cache, and then, if fails, the class object itself.

Throws:

java.lang.NoSuchMethodException

java.lang.SecurityException