JML

org.jmlspecs.jmlrac.runtime
Class JMLRacValue

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

Constructor Detail

JMLRacValue

private JMLRacValue(Object value)
Constructs a new instance. Note that the argument, value, may be null.


JMLRacValue

private JMLRacValue()
Constructs a new instance.

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(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

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.