fmrisc.ProgramExplorer.Judgements

Class Substitution

java.lang.Object

fmrisc.ProgramExplorer.Syntax.ASTVisitorBase

fmrisc.ProgramExplorer.Syntax.ASTCloner

fmrisc.ProgramExplorer.Judgements.Substitution

All Implemented Interfaces:

ASTVisitor

public final class Substitution
extends ASTCloner

The program variable substitution P[U1/VAR x,...]

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	Substitution.Action
static class	Substitution.Value The substitution for a reference to a program variable.

Method Summary

Methods

Modifier and Type	Method and Description
static Expression	perform(Expression exp, Term oldStateTerm, Term newStateTerm, java.util.Map<VariableSymbol,Substitution.Value> vars) Create a copy of expression with the denoted substitutions performed.
void	visit(NewState exp) Substitute expression.
void	visit(OldState exp) Substitute expression.
void	visit(PostVariable exp) Substitute expression.
void	visit(PreVariable exp) Substitute expression.

Methods inherited from class fmrisc.ProgramExplorer.Syntax.ASTCloner

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

Methods inherited from class fmrisc.ProgramExplorer.Syntax.ASTVisitorBase

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

Methods inherited from class java.lang.Object

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

Method Detail

perform

public static Expression perform(Expression exp,
                 Term oldStateTerm,
                 Term newStateTerm,
                 java.util.Map<VariableSymbol,Substitution.Value> vars)

Create a copy of expression with the denoted substitutions performed.

Parameters:

exp - the expression to be copied.

oldStateTerm - the substitution for "now" (if null, no substitution)

newStateTerm - the substitution for "next (if null, no substitution)

vars - the substitutions for (references to) program variables

Returns:

a copy of exp with the corresponding substitutions performed (only clones of the substitution terms are integrated into the copy)

visit

public void visit(OldState exp)

Substitute expression.

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

exp - the expression to be substituted.

visit

public void visit(NewState exp)

Substitute expression.

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

exp - the expression to be substituted.

visit

public void visit(PostVariable exp)

Substitute expression.

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

exp - the expression to be substituted.

visit

public void visit(PreVariable exp)

Substitute expression.

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

exp - the expression to be substituted.