public final class Normalization extends ASTCloner
Modifier and Type | Method and Description |
---|---|
static VariableSymbol |
modifiableVariable(Name name0)
Derive the modifiable variable from a name.
|
static java.util.Set<VariableSymbol> |
modifiableVariables(Name[] names)
Derive the modifiable variables of a method.
|
static void |
modifiableVariables(Name[] names,
java.util.Set<VariableSymbol> vars)
Derive the modifiable variables of a method.
|
static Formula |
perform(Formula formula)
Replace copy of formula with all poststate variables
replaced by prestate variables.
|
static Formula |
perform(Formula formula,
java.util.Collection<VariableSymbol> variables)
Replace copy of formula with all poststate variables that do not appear
in the set of modifiable variables replaced by prestate variables.
|
static Term |
perform(Term term)
Replace copy of term with all poststate variables
replaced by prestate variables.
|
static Formula |
postCondition(ParamSymbol method)
Get normalized postcondition of method (may be null).
|
static Formula |
preCondition(ParamSymbol method,
boolean init)
Get normalized precondition of method (may be null).
|
void |
visit(PostVariable exp)
Replace poststate variable by prestate variable if it
does not appear in the set of modifiable variables.
|
void |
visit(PreVariable exp)
Replace poststate variable by prestate variable if it
does not appear in the set of modifiable variables.
|
clone, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit
visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit
public static Formula perform(Formula formula)
formula
- the formula to be normalized.public static Term perform(Term term)
term
- the term to be normalized.public static Formula perform(Formula formula, java.util.Collection<VariableSymbol> variables)
formula
- the formula to be normalized.variables
- the set of modifiable variables.public static Formula preCondition(ParamSymbol method, boolean init)
method
- the method.init
- add initialization precondition to constructorspublic static Formula postCondition(ParamSymbol method)
method
- the method.public static java.util.Set<VariableSymbol> modifiableVariables(Name[] names)
names
- the names of the assignable clause of a method (may be null)public static void modifiableVariables(Name[] names, java.util.Set<VariableSymbol> vars)
names
- the names of the assignable clause of a method (may be null).vars
- a set to which the symbols of those variables are added
that may be modified according to the listed names.public static VariableSymbol modifiableVariable(Name name0)
name0
- the expression denoting the variable.public void visit(PostVariable exp)
visit
in interface ASTVisitor
visit
in class ASTCloner
exp
- the variable to be normalized.public void visit(PreVariable exp)
visit
in interface ASTVisitor
visit
in class ASTCloner
exp
- the variable to be normalized.