JML

org.multijava.mjc
Class CUniverseReadonly

java.lang.Object
  extended byorg.multijava.mjc.CUniverse
      extended byorg.multijava.mjc.CUniverseReadonly
Direct Known Subclasses:
CUniverseImplicitReadonly

public class CUniverseReadonly
extends CUniverse

Implements the readonly universe.

Author:
WMD

Field Summary
static byte byteConstant
          The constant used in the bytecode to represent this universe.
private static CUniverseReadonly instance
          The singleton readonly instance.
 
Constructor Summary
protected CUniverseReadonly()
           
 
Method Summary
 boolean equals(Object other)
          Any readonly reference equals other readonly or implicit-readonly references.
 byte getByteConstant()
          Returns the bytecode constant representing this particular universe.
static CUniverseReadonly getUniverse()
          Get an instance of the readonly universe.
 boolean isAlwaysAssignableTo(CUniverse other)
          A readonly reference is only assignable to another readonly reference.
 String toString()
          Return "readonly".
 
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

private static CUniverseReadonly instance
The singleton readonly instance.


byteConstant

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

Constructor Detail

CUniverseReadonly

protected CUniverseReadonly()
Method Detail

equals

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

Overrides:
equals in class CUniverse

isAlwaysAssignableTo

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


getUniverse

public static CUniverseReadonly getUniverse()
Get an instance of the readonly universe.


toString

public String toString()
Return "readonly".

Specified by:
toString in class CUniverse

getByteConstant

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


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.