JML

org.jmlspecs.jmlrac
Class RacContext

java.lang.Object
  extended byorg.jmlspecs.jmlrac.RacContext

public class RacContext
extends 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

Field Summary
private static int CTX_NEGATIVE
           
private static int CTX_POSITIVE
           
private  boolean enabled
          Indicates whether this context is enabled or not.
private  int type
          Type of this context.
 
Constructor Summary
private RacContext(int type)
          Construct a new context of the given type.
 
Method Summary
 String angelicValue(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.
 String demonicValue(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
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

CTX_POSITIVE

private static final int CTX_POSITIVE

CTX_NEGATIVE

private static final int CTX_NEGATIVE

type

private int type
Type of this context. It is either CTX_POSITIVE or CTX_POSITIVE.


enabled

private boolean enabled
Indicates whether this context is enabled or not.

Constructor Detail

RacContext

private RacContext(int type)
Construct a new context of the given type.

Parameters:
type - Type of context to create. It is either CTX_POSITIVE or CTX_POSITIVE.
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 String angelicValue(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 String demonicValue(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.


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.