fmrisc.ProgramExplorer.Judgements

Class Substitution.Value

java.lang.Object

fmrisc.ProgramExplorer.Judgements.Substitution.Value

Enclosing class:

Substitution

public static final class Substitution.Value
extends java.lang.Object

The substitution for a reference to a program variable.

Field Summary

Fields

Modifier and Type	Field and Description
Substitution.Action	postAction
Term	postTerm
Substitution.Action	preAction
Term	preTerm

Constructor Summary

Constructors

Constructor and Description
Value(Substitution.Action preAction, Term preTerm, Substitution.Action postAction, Term postTerm) Describe the substitution result of a program variable.

Method Summary

Methods inherited from class java.lang.Object

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

Field Detail

preAction

public final Substitution.Action preAction

preTerm

public final Term preTerm

postAction

public final Substitution.Action postAction

postTerm

public final Term postTerm

Constructor Detail

Value

public Value(Substitution.Action preAction,
             Term preTerm,
             Substitution.Action postAction,
             Term postTerm)

Describe the substitution result of a program variable.

Parameters:

preAction - the action on the pre-state value

preTerm - if preAction=term, then the replacement term

postAction - the action on the post-state value

postTerm - if postAction=term, then the replacement term