JML

org.jmlspecs.jmlrac.runtime
Class JMLSurrogate

java.lang.Object
  extended byorg.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.

Constructor Detail

JMLSurrogate

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

Method Detail

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

JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.