org.jmlspecs.jml4.rac
Class VariableGenerator

java.lang.Object
  org.jmlspecs.jml4.rac.VariableGenerator

public abstract class VariableGenerator
extends java.lang.Object

A class for generating various unique variable names for RAC.

Author:

Yoonsik Cheon and Amritam Sarcar

Constructor Summary

VariableGenerator()

Method Summary

abstract java.lang.String	currentStackVar()
static VariableGenerator	forClass() Return a variable generator for classes
static VariableGenerator	forMethod(VariableGenerator varGen) Return a variable generator for methods
abstract java.lang.String	freshCatchVar() Return a fresh variable name for use in a catch clause.
abstract java.lang.String	freshOldVar() Return a fresh variable name for storing the result of an old expression or an old variable.
abstract java.lang.String	freshPostVar() Return a fresh variable name for storing the result of evaluating a specification case of a precondition.
abstract java.lang.String	freshPreVar() Return a fresh variable name for storing the result of evaluating a specification case of a precondition.
abstract java.lang.String	freshStackVar() Return a fresh variable name for a stack for use as saving to and restoring from pre-state values for potential recursive method calls.
abstract java.lang.String	freshVar() Return a fresh variable name unique in the method.

Methods inherited from class java.lang.Object

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

Constructor Detail

VariableGenerator

public VariableGenerator()

Method Detail

forClass

public static VariableGenerator forClass()

Return a variable generator for classes

forMethod

public static VariableGenerator forMethod(VariableGenerator varGen)

Return a variable generator for methods

Parameters:

varGen - Variable generator for classes

freshOldVar

public abstract java.lang.String freshOldVar()

Return a fresh variable name for storing the result of an old expression or an old variable. The generated name is unique in the class. The returned name is of the form: VN_OLD_VAR + n, where n is a unique number.

See Also:

RacConstants.VN_OLD_VAR

freshPreVar

public abstract java.lang.String freshPreVar()

Return a fresh variable name for storing the result of evaluating a specification case of a precondition. The returned name is unique in the class. The returned name is of the form: VN_PRE_VAR + n, where n is a unique number.

See Also:

RacConstants.VN_PRE_VAR

freshPostVar

public abstract java.lang.String freshPostVar()

Return a fresh variable name for storing the result of evaluating a specification case of a precondition. The returned name is unique in the method and is of the form: VN_POST_VAR + n, where n is a unique number.

See Also:

RacConstants.VN_POST_VAR

freshStackVar

public abstract java.lang.String freshStackVar()

Return a fresh variable name for a stack for use as saving to and restoring from pre-state values for potential recursive method calls. The returned name is unique in the class. The returned name is of the form: VN_STACK_VAR + n, where n is a unique number.

See Also:

RacConstants.VN_STACK_VAR

currentStackVar

public abstract java.lang.String currentStackVar()

freshVar

public abstract java.lang.String freshVar()

Return a fresh variable name unique in the method. The returned name is of the form: VN_FREE_VAR + n, where n is a unique number.

See Also:

RacConstants.VN_FREE_VAR

freshCatchVar

public abstract java.lang.String freshCatchVar()

Return a fresh variable name for use in a catch clause. The returned name is unique in the method scope and of the form: VN_CATCH_VAR + n, where n is a unique number.

See Also:

RacConstants.VN_FREE_VAR