org.jmlspecs.jml4.rac.runtime
Class JMLRacValue

java.lang.Object
  org.jmlspecs.jml4.rac.runtime.JMLRacValue

public class JMLRacValue
extends java.lang.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

Method Summary

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(java.lang.Object v) Returns a new JMLRacValue object that wraps the given argument.
static JMLRacValue	ofUndefined() Returns an instance that denotes an angelic undefinedness.
java.lang.String	toString() Returns the string representation of this object.
java.lang.Object	value() Returns the wrapped value of this JMLRacValue object .

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

Method Detail

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(java.lang.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 java.lang.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.

toString

public java.lang.String toString()

Returns the string representation of this object.

Overrides:

toString in class java.lang.Object