de.uka.ilkd.key.symbolic_execution

Class ExecutionNodeReader.KeYlessJoin

java.lang.Object

de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.AbstractKeYlessExecutionElement

de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.AbstractKeYlessExecutionNode<SourceElement>

de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.KeYlessJoin

All Implemented Interfaces:

IExecutionElement, IExecutionJoin, IExecutionNode<SourceElement>

Enclosing class:

ExecutionNodeReader

public static class ExecutionNodeReader.KeYlessJoin
extends ExecutionNodeReader.AbstractKeYlessExecutionNode<SourceElement>
implements IExecutionJoin

An implementation of IExecutionJoin which is independent from KeY and provides such only children and default attributes.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private boolean	weakeningVerified Is the weakening verified?

Fields inherited from interface de.uka.ilkd.key.symbolic_execution.model.IExecutionNode

INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START

Constructor Summary

Constructors

Constructor and Description
KeYlessJoin(IExecutionNode<?> parent, java.lang.String name, java.lang.String formatedPathCondition, boolean pathConditionChanged, boolean weakeningVerified) Constructor.

Method Summary

Modifier and Type	Method and Description
java.lang.String	getElementType() Returns a human readable element type name.
boolean	isWeakeningVerificationSupported() Checks if the weakening verification is supported.
boolean	isWeakeningVerified() Checks if the weakening is verified.

Methods inherited from class de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.AbstractKeYlessExecutionNode

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

Methods inherited from class de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.AbstractKeYlessExecutionElement

getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, toString

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Methods inherited from interface de.uka.ilkd.key.symbolic_execution.model.IExecutionNode

getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getOutgoingLink, getOutgoingLinks, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged

Methods inherited from interface de.uka.ilkd.key.symbolic_execution.model.IExecutionElement

getAppliedRuleApp, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed

Field Detail

weakeningVerified

private final boolean weakeningVerified

Is the weakening verified?

Constructor Detail

KeYlessJoin

public KeYlessJoin(IExecutionNode<?> parent,
                   java.lang.String name,
                   java.lang.String formatedPathCondition,
                   boolean pathConditionChanged,
                   boolean weakeningVerified)

Constructor.

Parameters:

parent - The parent IExecutionNode.

name - The name of this node.

pathConditionChanged - Is the path condition changed compared to parent?

formatedPathCondition - The formated path condition.

weakeningVerified - Is the weakening verified?

Method Detail

getElementType

public java.lang.String getElementType()

Returns a human readable element type name.

Specified by:

getElementType in interface IExecutionElement

Returns:

The human readable element type.

isWeakeningVerified

public boolean isWeakeningVerified()

Checks if the weakening is verified.

Specified by:

isWeakeningVerified in interface IExecutionJoin

Returns:

true is verified, false is not verified.

isWeakeningVerificationSupported

public boolean isWeakeningVerificationSupported()

Checks if the weakening verification is supported.

Specified by:

isWeakeningVerificationSupported in interface IExecutionJoin

Returns:

true supported, false not supported.