org.jmlspecs.models
Class JMLModelObjectSet

java.lang.Object
  org.jmlspecs.models.JMLModelObjectSet

public class JMLModelObjectSet

extends Object

A collection of object sets for use in set comprehensions. All of the public methods are model methods, because there is no way to compute the set of all potential object identities of any given type.

This type is not that useful, as you can mostly just use quantification over the relevant type instead of one of these sets. Indeed the sets are defined by using universal quantifiers, and so their use is roughly equivalent.

Version:

$Revision: 1.13 $

Author:

Gary T. Leavens

Class Specifications

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Model Field Summary

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Constructor Summary
private	JMLModelObjectSet()           This class has no instances.

 

Model Method Summary
static JMLObjectSet	Booleans()           The set of all (actual and potential) Boolean objects.
static JMLObjectSet	Bytes()           The set of all (actual and potential) Byte objects.
static JMLObjectSet	Characters()           The set of all (actual and potential) Character objects.
static JMLObjectSet	Doubles()           The set of all (actual and potential) Double objects.
static JMLObjectSet	Floats()           The set of all (actual and potential) Float objects.
static JMLObjectSet	Integers()           The set of all (actual and potential) Integer objects.
static JMLObjectSet	JMLBytes()           The set of all (actual and potential) JMLByte objects.
static JMLObjectSet	JMLChars()           The set of all (actual and potential) JMLChar objects.
static JMLObjectSet	JMLDoubles()           The set of all (actual and potential) JMLDouble objects.
static JMLObjectSet	JMLFloats()           The set of all (actual and potential) JMLFloat objects.
static JMLObjectSet	JMLIntegers()           The set of all (actual and potential) JMLInteger objects.
static JMLObjectSet	JMLLongs()           The set of all (actual and potential) JMLLong objects.
static JMLObjectSet	JMLShorts()           The set of all (actual and potential) JMLShort objects.
static JMLObjectSet	JMLStrings()           The set of all (actual and potential) JMLString objects.
static JMLObjectSet	Longs()           The set of all (actual and potential) Long objects.
static JMLObjectSet	Shorts()           The set of all (actual and potential) Short objects.
static JMLObjectSet	Strings()           The set of all (actual and potential) String objects.

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary

 

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

 

Constructor Detail

JMLModelObjectSet

private JMLModelObjectSet()

This class has no instances.

Specifications: (class)pure

JMLBytes

public static JMLObjectSet JMLBytes()

The set of all (actual and potential) JMLByte objects.

Specifications: pure non_null

public normal_behavior
assignable \nothing;
ensures ( \forall org.jmlspecs.models.JMLByte x; ; \result .has(x));

JMLChars

public static JMLObjectSet JMLChars()

The set of all (actual and potential) JMLChar objects.

Specifications: pure non_null

public normal_behavior
assignable \nothing;
ensures ( \forall org.jmlspecs.models.JMLChar x; ; \result .has(x));

JMLIntegers

public static JMLObjectSet JMLIntegers()

The set of all (actual and potential) JMLInteger objects.

Specifications: pure non_null

public normal_behavior
assignable \nothing;
ensures ( \forall org.jmlspecs.models.JMLInteger x; ; \result .has(x));

JMLLongs

public static JMLObjectSet JMLLongs()

The set of all (actual and potential) JMLLong objects.

Specifications: pure non_null

public normal_behavior
assignable \nothing;
ensures ( \forall org.jmlspecs.models.JMLLong x; ; \result .has(x));

JMLShorts

public static JMLObjectSet JMLShorts()

The set of all (actual and potential) JMLShort objects.

Specifications: pure non_null

public normal_behavior
assignable \nothing;
ensures ( \forall org.jmlspecs.models.JMLShort x; ; \result .has(x));

JMLStrings

public static JMLObjectSet JMLStrings()

The set of all (actual and potential) JMLString objects.

Specifications: pure non_null

public normal_behavior
assignable \nothing;
ensures ( \forall org.jmlspecs.models.JMLString x; ; \result .has(x));

JMLFloats

public static JMLObjectSet JMLFloats()

The set of all (actual and potential) JMLFloat objects.

Specifications: pure non_null

public normal_behavior
assignable \nothing;
ensures ( \forall org.jmlspecs.models.JMLFloat x; ; \result .has(x));

JMLDoubles

public static JMLObjectSet JMLDoubles()

The set of all (actual and potential) JMLDouble objects.

Specifications: pure non_null

public normal_behavior
assignable \nothing;
ensures ( \forall org.jmlspecs.models.JMLDouble x; ; \result .has(x));

Booleans

public static JMLObjectSet Booleans()

The set of all (actual and potential) Boolean objects.

Specifications: pure non_null

public normal_behavior
assignable \nothing;
ensures ( \forall java.lang.Boolean x; ; \result .has(x));

Bytes

public static JMLObjectSet Bytes()

The set of all (actual and potential) Byte objects.

Specifications: pure non_null

public normal_behavior
assignable \nothing;
ensures ( \forall java.lang.Byte x; ; \result .has(x));

Characters

public static JMLObjectSet Characters()

The set of all (actual and potential) Character objects.

Specifications: pure non_null

public normal_behavior
assignable \nothing;
ensures ( \forall java.lang.Character x; ; \result .has(x));

Integers

public static JMLObjectSet Integers()

The set of all (actual and potential) Integer objects.

Specifications: pure non_null

public normal_behavior
assignable \nothing;
ensures ( \forall java.lang.Integer x; ; \result .has(x));

Longs

public static JMLObjectSet Longs()

The set of all (actual and potential) Long objects.

Specifications: pure non_null

public normal_behavior
assignable \nothing;
ensures ( \forall java.lang.Long x; ; \result .has(x));

Shorts

public static JMLObjectSet Shorts()

The set of all (actual and potential) Short objects.

Specifications: pure non_null

public normal_behavior
assignable \nothing;
ensures ( \forall java.lang.Short x; ; \result .has(x));

Strings

public static JMLObjectSet Strings()

The set of all (actual and potential) String objects.

Specifications: pure non_null

public normal_behavior
assignable \nothing;
ensures ( \forall java.lang.String x; ; \result .has(x));

Floats

public static JMLObjectSet Floats()

The set of all (actual and potential) Float objects.

Specifications: pure non_null

public normal_behavior
assignable \nothing;
ensures ( \forall java.lang.Float x; ; \result .has(x));

Doubles

public static JMLObjectSet Doubles()

The set of all (actual and potential) Double objects.

Specifications: pure non_null

public normal_behavior
assignable \nothing;
ensures ( \forall java.lang.Double x; ; \result .has(x));