public static class ExecutionNodeReader.KeYlessBlockContract extends ExecutionNodeReader.AbstractKeYlessExecutionNode<SourceElement> implements IExecutionAuxiliaryContract
IExecutionAuxiliaryContract
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 |
---|
KeYlessBlockContract(IExecutionNode<?> parent,
java.lang.String name,
java.lang.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
AuxiliaryContract . |
java.lang.String |
getElementType()
Returns a human readable element type name.
|
boolean |
isPreconditionComplied()
Checks if the precondition is complied.
|
addCallStackEntry, addChild, addCompletedBlock, addConstraint, addIncomingLink, addOutgoingLink, addVariable, getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getModalityPIO, getOutgoingLink, getOutgoingLinks, 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, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getOutgoingLink, getOutgoingLinks, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged
getAppliedRuleApp, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
public KeYlessBlockContract(IExecutionNode<?> parent, java.lang.String name, java.lang.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 java.lang.String getElementType()
getElementType
in interface IExecutionElement
public BlockContract getContract()
AuxiliaryContract
.getContract
in interface IExecutionAuxiliaryContract
AuxiliaryContract
.public StatementBlock getBlock()
StatementBlock
at which the BlockContract
is applied.getBlock
in interface IExecutionAuxiliaryContract
StatementBlock
at which the BlockContract
is applied.public boolean isPreconditionComplied()
isPreconditionComplied
in interface IExecutionAuxiliaryContract
true
precondition complied, false
precondition not complied.