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

Nested Class Summary
private static class JMLSurrogate.MapKey
          A class for implementing keys for the method cache.
 
Field Summary
static Map methods
          The shared cache for dynamically looking up 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(JMLCheckable self)
          Constructs a new surrogate for the given object, obj.
 
Method Summary
static Method getAccessor(Class clazz, String name)
          Returns the accessor (getter) method of a ghost field or a model field, name, declared in the type, clazz.
static Method getMethod(Class clazz, 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(Class clazz, String name, 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
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);
 


self

protected JMLCheckable self
object that this object is surrogate for.


NULL_METHOD

private static final Object NULL_METHOD
A special object denoting no method.

Constructor Detail

JMLSurrogate

protected JMLSurrogate(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(Class clazz,
                               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

getAccessor

public static Method getAccessor(Class clazz,
                                 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

getSetter

public static Method getSetter(Class clazz,
                               String name,
                               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

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.