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

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

 

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.

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

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.

Specifications: non_null

ofNonExecutable

public static JMLRacValue ofNonExecutable()

Returns an instance that denotes a demonic undefinedness.

Specifications: non_null

ofObject

public static JMLRacValue ofObject(Object v)

Returns a new JMLRacValue object that wraps the given argument.

Specifications: non_null

ofBoolean

public static JMLRacValue ofBoolean(boolean v)

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

Specifications: non_null

ofInt

public static JMLRacValue ofInt(int v)

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

Specifications: non_null

value

public Object value()

Returns the wrapped value of this JMLRacValue object .

Specifications: pure

isAngel

public boolean isAngel()

Returns true if this object represents an angelic undefinedness.

Specifications: pure

isDemon

public boolean isDemon()

Returns true if this object represents a demonic undefinedness.

Specifications: pure

checkUndefinedness

private void checkUndefinedness()

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

Specifications: pure

toString

public String toString()

Returns the string representation of this object.

Overrides:

toString in class Object

Specifications: pure non_null

Specifications inherited from overridden method in class Object:
       non_null

public normal_behavior
assignable objectState;
ensures \result != null&&\result .equals(this.theString);
ensures (* \result is a string representation of this object *);

     also

public code normal_behavior
assignable \nothing;
ensures \result != null&&(* \result is the instance's class name, followed by an @, followed by the instance's hashcode in hex *);

     also

public code model_program { ... }

    implies_that

assignable objectState;
ensures \result != null;