JML

org.jmlspecs.models
Class JMLModelObjectSet

java.lang.Object
  extended byorg.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
Model Method Detail

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));

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.