JML

org.multijava.mjc
Class CUniverse

java.lang.Object
  extended byorg.multijava.mjc.CUniverse
Direct Known Subclasses:
CUniversePeer, CUniverseReadonly, CUniverseRep

public abstract class CUniverse
extends Object

This is the abstract base class that represents Universes. It defines some standard methods and most importantly implements the Type-Scheme combinator in the method combine.

Author:
WMD

Constructor Summary
protected CUniverse()
           
 
Method Summary
static CUniverse combine(CUniverse first, CUniverse second)
          Combine two given universes and return the result universe.
 boolean equals(Object other)
          Check whether two universe objects are the same.
abstract  byte getByteConstant()
          Returns the bytecode constant representing this particular universe.
abstract  boolean isAlwaysAssignableTo(CUniverse other)
          Tests whether the current universe can be assigned to the given universe.
 String toJMLString()
          Output the name of the universe as it should be used for JML code.
 String toMJString()
          Output the name of the universe as it should be used for MJ code.
abstract  String toString()
          Output the name of the universe.
 
Methods inherited from class java.lang.Object
clone, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Constructor Detail

CUniverse

protected CUniverse()
Method Detail

equals

public boolean equals(Object other)
Check whether two universe objects are the same. For now we simply look whether it's a universe of the same class. FIXME.

Overrides:
equals in class Object

isAlwaysAssignableTo

public abstract boolean isAlwaysAssignableTo(CUniverse other)
Tests whether the current universe can be assigned to the given universe.

Parameters:
other - The destination universe type.

toString

public abstract String toString()
Output the name of the universe.

Overrides:
toString in class Object

toMJString

public String toMJString()
Output the name of the universe as it should be used for MJ code.


toJMLString

public String toJMLString()
Output the name of the universe as it should be used for JML code.


getByteConstant

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


combine

public static CUniverse combine(CUniverse first,
                                CUniverse second)
Combine two given universes and return the result universe.

Parameters:
first - The first/left hand side universe.
second - The second/right hand side universe.
Returns:
The combined result 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.