org.jmlspecs.jmlrac.runtime
Class JMLRacValue

java.lang.Object
  org.jmlspecs.jmlrac.runtime.JMLRacValue

public class JMLRacValue

extends Object

A class for denoting JML expressible values for the runtime assertion checker. In addition to regular Java values and objects, this class can represent two special JML values: undefinedness and non-executability. An undefined value denotes the value of an expression that throws an exception during evaluation. Similarly, a non-executable value denotes a non-executable JML expression.

Version:

$Revision: 1.4 $

Author:

Yoonsik Cheon

Field Summary
private static JMLRacValue	ANGEL           A unique object to represent an angelic undefinedness such as non-executable specification constructs.
private static JMLRacValue	DEMON           A unique object to represent a demonic undefinedness such as runtime exceptions.
private  Object	value           The object wrapped by this instance of class JMLRacValue.

 

Constructor Summary
private	JMLRacValue()           Constructs a new instance.
private	JMLRacValue(Object value)           Constructs a new instance.

 

Method Summary
private  void	checkUndefinedness()           Throws appropriate exception if this object represents either angelic or demonic undefinedness.
boolean	isAngel()           Returns true if this object represents an angelic undefinedness.
boolean	isDemon()           Returns true if this object represents a demonic undefinedness.
static JMLRacValue	ofBoolean(boolean v)           Returns a new JMLRacValue object that wraps the given boolean value, v.
static JMLRacValue	ofInt(int v)           Returns a new JMLRacValue object that wraps the given int value, v.
static JMLRacValue	ofNonExecutable()           Returns an instance that denotes a demonic undefinedness.
static JMLRacValue	ofObject(Object v)           Returns a new JMLRacValue object that wraps the given argument.
static JMLRacValue	ofUndefined()           Returns an instance that denotes an angelic undefinedness.
String	toString()           Returns the string representation of this object.
Object	value()           Returns the wrapped value of this JMLRacValue object .

 

Methods inherited from class java.lang.Object

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

 

Field Detail

ANGEL

private static final JMLRacValue ANGEL

A unique object to represent an angelic undefinedness such as non-executable specification constructs.

DEMON

private static final JMLRacValue DEMON

A unique object to represent a demonic undefinedness such as runtime exceptions.

value

private Object value

The object wrapped by this instance of class JMLRacValue. Note that it may be null.

JMLRacValue

private JMLRacValue(Object value)

Constructs a new instance. Note that the argument, value, may be null.

JMLRacValue

private JMLRacValue()

Constructs a new instance.

ofUndefined

public static JMLRacValue ofUndefined()

Returns an instance that denotes an angelic undefinedness.

ofNonExecutable

public static JMLRacValue ofNonExecutable()

Returns an instance that denotes a demonic undefinedness.

ofObject

public static JMLRacValue ofObject(Object v)

Returns a new JMLRacValue object that wraps the given argument.

ofBoolean

public static JMLRacValue ofBoolean(boolean v)

Returns a new JMLRacValue object that wraps the given boolean value, v.

ofInt

public static JMLRacValue ofInt(int v)

Returns a new JMLRacValue object that wraps the given int value, v.

value

public Object value()

Returns the wrapped value of this JMLRacValue object .

isAngel

public boolean isAngel()

Returns true if this object represents an angelic undefinedness.

isDemon

public boolean isDemon()

Returns true if this object represents a demonic undefinedness.

checkUndefinedness

private void checkUndefinedness()

Throws appropriate exception if this object represents either angelic or demonic undefinedness.

toString

public String toString()

Returns the string representation of this object.

Overrides:

toString in class Object