JML

org.multijava.mjc
Class CUniversePeer

java.lang.Object
  extended byorg.multijava.mjc.CUniverse
      extended byorg.multijava.mjc.CUniversePeer
Direct Known Subclasses:
CUniverseImplicitPeer

public class CUniversePeer
extends CUniverse

This class implements a peer/ground/default universe. This is the standard universe that is used if no special annotation is given.

Author:
WMD

Field Summary
static byte byteConstant
          The constant used in the bytecode to represent this universe.
static CUniversePeer instance
          The singleton reference.
 
Constructor Summary
CUniversePeer()
           
 
Method Summary
 boolean equals(Object other)
          Any peer reference equals other peer or implicit-peer references.
 byte getByteConstant()
          Returns the bytecode constant representing this particular universe.
static CUniversePeer getUniverse()
          Factory method to return the single universe instance.
 boolean isAlwaysAssignableTo(CUniverse other)
          A peer is only assignable to another peer or to a readonly reference.
 String toString()
          Output "peer".
 
Methods inherited from class org.multijava.mjc.CUniverse
combine, toJMLString, toMJString
 
Methods inherited from class java.lang.Object
clone, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Field Detail

instance

public static CUniversePeer instance
The singleton reference.


byteConstant

public static final byte byteConstant
The constant used in the bytecode to represent this universe.

Constructor Detail

CUniversePeer

public CUniversePeer()
Method Detail

equals

public boolean equals(Object other)
Any peer reference equals other peer or implicit-peer references.

Overrides:
equals in class CUniverse

isAlwaysAssignableTo

public boolean isAlwaysAssignableTo(CUniverse other)
A peer is only assignable to another peer or to a readonly reference.


toString

public String toString()
Output "peer".

Specified by:
toString in class CUniverse

getByteConstant

public byte getByteConstant()
Returns the bytecode constant representing this particular universe.


getUniverse

public static CUniversePeer getUniverse()
Factory method to return the single universe instance. This might be changed later to have multiple different peer universes.


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.