org.jmlspecs.jml4.rac.quantifiedexpression
Class RacContext

java.lang.Object
  org.jmlspecs.jml4.rac.quantifiedexpression.RacContext

public class RacContext
extends java.lang.Object

A class for representing contexts for translating JML expressions. A translation context can be either positive or negative. In a positive context, JML expressions are translated in such a way as to interpret runtime exceptions thrown by the expressions as false. In a negative context, the exceptions are interpreted as true. If a context is disabled, no interpretation is made, i.e., exceptions are further propagated into the enclosing expression.

Version:

$Revision: 1.4 $

Author:

Yoonsik Cheon

Method Summary

java.lang.String	angelicValue(java.lang.String var) Returns the string form of statement expression that sets the variable, var, to the value for an angelic undefinedness.
void	changePolarity() Changes the type of this context.
static RacContext	createNegative() Returns a new negative context.
static RacContext	createNeutral() Returns a new neutral context.
static RacContext	createOpposite(RacContext ctx) Returns a new context that has the opposite polarity to the given context, but with the same status.
static RacContext	createPositive() Returns a new positive context.
java.lang.String	demonicValue(java.lang.String var) Returns the string form of statement expression that sets the variable, var, to the value for an demonic undefinedness.
void	disable() Disables contextual interpretation.
void	enable() Enables contextual interpretation.
boolean	enabled() Returns true if contextual interpretation is enabled.
boolean	isNegative() Returns true if this context is a negative context.
boolean	isPositive() Returns true if this context is a positive context.
void	setEnabled(boolean status) Enables or diables contextual interpretation.

Methods inherited from class java.lang.Object

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

Method Detail

createPositive

public static RacContext createPositive()

Returns a new positive context.

createNegative

public static RacContext createNegative()

Returns a new negative context.

createNeutral

public static RacContext createNeutral()

Returns a new neutral context. A neutral contex is a positive context, but disabled.

createOpposite

public static RacContext createOpposite(RacContext ctx)

Returns a new context that has the opposite polarity to the given context, but with the same status.

isPositive

public boolean isPositive()

Returns true if this context is a positive context.

isNegative

public boolean isNegative()

Returns true if this context is a negative context.

angelicValue

public java.lang.String angelicValue(java.lang.String var)

Returns the string form of statement expression that sets the variable, var, to the value for an angelic undefinedness. For example, return value is var + " = true" for a positive context and var + " = false for a negative context. It is "throw new JMLNonExecutableException()" if this context is disabled.

demonicValue

public java.lang.String demonicValue(java.lang.String var)

Returns the string form of statement expression that sets the variable, var, to the value for an demonic undefinedness. For example, return value is var + " = false" for a positive context and var + " = true for a negative context. It is "throw new RuntimeException()" if this context is disabled.

enabled

public boolean enabled()

Returns true if contextual interpretation is enabled.

enable

public void enable()

Enables contextual interpretation.

disable

public void disable()

Disables contextual interpretation.

changePolarity

public void changePolarity()

Changes the type of this context. E.g., from positive to negative, or negative to positive.

setEnabled

public void setEnabled(boolean status)

Enables or diables contextual interpretation.