org.jmlspecs.jmlrac.runtime
Class JMLSurrogate

java.lang.Object
  org.jmlspecs.jmlrac.runtime.JMLSurrogate

public abstract class JMLSurrogate

extends 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

Class Specifications

public invariant org.jmlspecs.jmlrac.runtime.JMLSurrogate.methods != null&&( \forall org.jmlspecs.jmlrac.runtime.JMLSurrogate.MapKey k; org.jmlspecs.jmlrac.runtime.JMLSurrogate.methods.containsKey(k); org.jmlspecs.jmlrac.runtime.JMLSurrogate.methods.get(k) instanceof java.lang.reflect.Method);

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Nested Class Summary
[spec_public] private static class	JMLSurrogate.MapKey           A class for implementing keys for the method cache.

 

Model Field Summary

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Field Summary
static Map	methods
private static Object	NULL_METHOD           A special object denoting no method.
protected  JMLCheckable	self           object that this object is surrogate for.

 

Constructor Summary
protected	JMLSurrogate(non_null JMLCheckable self)           Constructs a new surrogate for the given object, obj.

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
static Method	getAccessor(non_null Class clazz, non_null String name)           Returns the accessor (getter) method of a ghost field or a model field, name, declared in the type, clazz.
static Method	getMethod(non_null Class clazz, non_null String name, Class[] types)           Returns a method object that reflects the specified public member method of the class or interface, clazz.
protected static Object	getReceiver(Class clazz, Object thisObj)           Returns the receiver object for dynamic calls to methods of the class clazz from the object thisObj.
JMLCheckable	getSelf()           Returns the delegee of this object.
static Method	getSetter(non_null Class clazz, non_null String name, non_null 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

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

 

Field Detail

methods

public static final Map methods

self

protected JMLCheckable self

object that this object is surrogate for.

Specifications: non_null

NULL_METHOD

private static final Object NULL_METHOD

A special object denoting no method.

JMLSurrogate

protected JMLSurrogate(non_null JMLCheckable self)

Constructs a new surrogate for the given object, obj.

getSelf

public JMLCheckable getSelf()

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

getReceiver

protected static Object getReceiver(Class clazz,
                                    Object thisObj)

Returns the receiver object for dynamic calls to methods of the class clazz from the object thisObj. If the object thisObj is a surrogate object, its delegee is referenced to determine an existing, appropriate object or create a new one; otherwise, the object itself is the receiver.

getMethod

public static Method getMethod(non_null Class clazz,
                               non_null String name,
                               Class[] types)
                        throws NoSuchMethodException,
                               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:

NoSuchMethodException

SecurityException

Specifications: non_null

getAccessor

public static Method getAccessor(non_null Class clazz,
                                 non_null String name)
                          throws NoSuchMethodException,
                                 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:

NoSuchMethodException

SecurityException

Specifications: non_null

getSetter

public static Method getSetter(non_null Class clazz,
                               non_null String name,
                               non_null Class type)
                        throws NoSuchMethodException,
                               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:

NoSuchMethodException

SecurityException

Specifications: non_null