public static class ExecutionNodeReader.KeYlessBlockContract extends ExecutionNodeReader.AbstractKeYlessExecutionNode<SourceElement> implements IExecutionBlockContract
IExecutionBlockContract
which is independent
from KeY and provides such only children and default attributes.Modifier and Type | Field and Description |
---|---|
private boolean |
preconditionComplied
Precondition complied?
|
INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
Constructor and Description |
---|
ExecutionNodeReader.KeYlessBlockContract(IExecutionNode<?> parent,
String name,
String formatedPathCondition,
boolean pathConditionChanged,
boolean preconditionComplied)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
StatementBlock |
getBlock()
Returns the
StatementBlock at which the BlockContract is applied. |
BlockContract |
getContract()
Returns the applied
BlockContract . |
String |
getElementType()
Returns a human readable element type name.
|
boolean |
isPreconditionComplied()
Checks if the precondition is complied.
|
addCallStackEntry, addChild, addCompletedBlock, addConstraint, addVariable, getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getModalityPIO, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged
getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, toString
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged
getAppliedRuleApp, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
public ExecutionNodeReader.KeYlessBlockContract(IExecutionNode<?> parent, String name, String formatedPathCondition, boolean pathConditionChanged, boolean preconditionComplied)
parent
- The parent IExecutionNode
.name
- The name of this node.pathConditionChanged
- Is the path condition changed compared to parent?formatedPathCondition
- The formated path condition.preconditionComplied
- Precondition complied?public String getElementType()
getElementType
in interface IExecutionElement
public BlockContract getContract()
BlockContract
.getContract
in interface IExecutionBlockContract
BlockContract
.public StatementBlock getBlock()
StatementBlock
at which the BlockContract
is applied.getBlock
in interface IExecutionBlockContract
StatementBlock
at which the BlockContract
is applied.public boolean isPreconditionComplied()
isPreconditionComplied
in interface IExecutionBlockContract
true
precondition complied, false
precondition not complied.