org.jmlspecs.lang
Class JMLDataGroup

java.lang.Object
  org.jmlspecs.lang.JMLDataGroup

public final class JMLDataGroup

extends Object

A type with one element, for use in declaring "data groups". Note that there is only one equivalence class of objects of this type; that is, all objects of this type are considered .equal to each other.

Version:

$Revision: 1.4 $

Author:

Gary T. Leavens, based on an idea of Rustan Leino

Field Summary
static JMLDataGroup	IT           The only object of this type.

 

Constructor Summary
private	JMLDataGroup()           Initialize this object.

 

Method Summary
Object	clone()           Return this object.
boolean	equals(Object oth)           Test whether the given argument is a non-null object of type JMLDataGroup.
int	hashCode()           Return a hash code for this object.
String	toString()           Return a string representation of this object.

 

Methods inherited from class java.lang.Object

finalize, getClass, notify, notifyAll, wait, wait, wait

 

Field Detail

IT

public static final JMLDataGroup IT

The only object of this type.

JMLDataGroup

private JMLDataGroup()

Initialize this object.

See Also:

IT

clone

public Object clone()

Return this object.

Overrides:

clone in class Object

equals

public boolean equals(Object oth)

Test whether the given argument is a non-null object of type JMLDataGroup.

Overrides:

equals in class Object

hashCode

public int hashCode()

Return a hash code for this object.

Overrides:

hashCode in class Object

toString

public String toString()

Return a string representation of this object.

Overrides:

toString in class Object