Modifier and Type | Field and Description |
---|---|
boolean |
breaks |
boolean |
continues |
java.util.Set<ClassSymbol> |
exceptions |
boolean |
executes |
Formula |
formula |
boolean |
returns |
Formula |
sformula |
java.util.Set<VariableSymbol> |
variables |
Constructor and Description |
---|
StatJudgement(Formula precondition,
Formula formula,
boolean executes,
boolean continues,
boolean breaks,
boolean returns,
java.util.Set<ClassSymbol> exceptions,
java.util.Set<VariableSymbol> variables)
Construct a command specification.
|
Modifier and Type | Method and Description |
---|---|
void |
accept(ASTVisitor visitor)
Accept visitor for a visit.
|
void |
accept(ASTVisitorOld visitor)
Accept visitor for a visit.
|
void |
acceptChildren(ASTVisitor visitor)
Accept visitor for a visit.
|
Formula |
getPrecondition()
Get the precondition formula.
|
Formula |
getTermination()
Get the termination formula.
|
void |
setPrecondition(Formula pre)
Get the precondition formula.
|
void |
setTermination(Formula termination)
Set the termination formula.
|
public final Formula formula
public final Formula sformula
public final boolean executes
public final boolean continues
public final boolean breaks
public final boolean returns
public final java.util.Set<ClassSymbol> exceptions
public final java.util.Set<VariableSymbol> variables
public StatJudgement(Formula precondition, Formula formula, boolean executes, boolean continues, boolean breaks, boolean returns, java.util.Set<ClassSymbol> exceptions, java.util.Set<VariableSymbol> variables)
precondition
- the formula describing the precondition (may be null).formula
- the formula describing the transition relation.executes
- true if the command may execute normally.continues
- true if the command may "continue".breaks
- true if the command may "break".returns
- true if the command may "return".exceptions
- the set of exceptions that may be thrown by the command
(null means the empty set)variables
- the set of variables that may be modified by the command
(null means the empty set)public void setTermination(Formula termination)
termination
- the formula.public Formula getTermination()
public void setPrecondition(Formula pre)
pre
- the formula.public Formula getPrecondition()
public void accept(ASTVisitorOld visitor)
public void accept(ASTVisitor visitor)
public void acceptChildren(ASTVisitor visitor)
acceptChildren
in interface AST
acceptChildren
in class ASTBase
visitor
- the visitor who is accepted by this node.