org.jmlspecs.models
Class JMLModelValueSet

java.lang.Object
  org.jmlspecs.models.JMLModelValueSet

public class JMLModelValueSet

extends Object

A collection of value sets for use in set comprehensions. The normal (non-model) methods might potentially be useful in executing assertions, although the sets of all integers and longs can't realistically be used in a direct way. The model methods have no hope of being executed.

Version:

$Revision: 1.6 $

Author:

Gary T. Leavens

See Also:

JMLValueSet

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	JMLModelValueSet()           This class has no instances.

 

Model Method Summary
static JMLValueSet	JMLDoubles()           The set of all (actual and potential) JMLDouble values.
static JMLValueSet	JMLFloats()           The set of all (actual and potential) JMLFloat values.
static JMLValueSet	JMLIntegers()           The set of all (actual and potential) JMLInteger values.
static JMLValueSet	JMLLongs()           The set of all (actual and potential) JMLLong values.
static JMLValueSet	JMLStrings()           The set of all (actual and potential) JMLString values.

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
static JMLValueSet	JMLBytes()           The set of all (actual and potential) JMLByte values.
static JMLValueSet	JMLChars()           The set of all (actual and potential) JMLChar values.
static JMLValueSet	JMLShorts()           The set of all (actual and potential) JMLShort values.

 

Methods inherited from class java.lang.Object

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

 

Constructor Detail

JMLModelValueSet

private JMLModelValueSet()

This class has no instances.

Specifications: (class)pure

JMLIntegers

public static JMLValueSet JMLIntegers()

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

Specifications: pure non_null

public normal_behavior
assignable \nothing;
ensures ( \forall int i; ; ( \exists org.jmlspecs.models.JMLInteger j; \result .has(j)&&j != null; j.theInt == i));

JMLLongs

public static JMLValueSet JMLLongs()

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

Specifications: pure non_null

public normal_behavior
assignable \nothing;
ensures ( \forall long i; ; ( \exists org.jmlspecs.models.JMLLong j; \result .has(j)&&j != null; j.theLong == i));

JMLStrings

public static JMLValueSet JMLStrings()

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

Specifications: pure non_null

public normal_behavior
assignable \nothing;
ensures ( \forall java.lang.String s; s != null; ( \exists org.jmlspecs.models.JMLString js; \result .has(js)&&js != null; js.theString.equals(s)));

JMLFloats

public static JMLValueSet JMLFloats()

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

Specifications: pure non_null

public normal_behavior
assignable \nothing;
ensures ( \forall float f; ; ( \exists org.jmlspecs.models.JMLFloat jf; \result .has(jf)&&jf != null; (java.lang.Float.isNaN(f)&&jf.isNaN())||jf.theFloat == f));

JMLDoubles

public static JMLValueSet JMLDoubles()

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

Specifications: pure non_null

public normal_behavior
assignable \nothing;
ensures ( \forall double f; ; ( \exists org.jmlspecs.models.JMLDouble jf; \result .has(jf)&&jf != null; (java.lang.Double.isNaN(f)&&jf.isNaN())||jf.theDouble == f));

JMLBytes

public static JMLValueSet JMLBytes()

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

Specifications: pure non_null

public normal_behavior
assignable \nothing;
ensures ( \forall byte i; ; ( \exists org.jmlspecs.models.JMLByte j; \result .has(j)&&j != null; j.theByte == i));

JMLChars

public static JMLValueSet JMLChars()

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

Specifications: pure non_null

public normal_behavior
assignable \nothing;
ensures ( \forall char i; ; ( \exists org.jmlspecs.models.JMLChar j; \result .has(j)&&j != null; j.theChar == i));

JMLShorts

public static JMLValueSet JMLShorts()

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

Specifications: pure non_null

public normal_behavior
assignable \nothing;
ensures ( \forall short i; ; ( \exists org.jmlspecs.models.JMLShort j; \result .has(j)&&j != null; j.theShort == i));