de.uka.ilkd.key.symbolic_execution.model.impl

Class ExecutionConstraint

java.lang.Object

de.uka.ilkd.key.symbolic_execution.model.impl.AbstractExecutionElement

de.uka.ilkd.key.symbolic_execution.model.impl.ExecutionConstraint

All Implemented Interfaces:

IExecutionConstraint, IExecutionElement

public class ExecutionConstraint
extends AbstractExecutionElement
implements IExecutionConstraint

The default implementation of IExecutionConstraint.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private PosInOccurrence	modalityPIO The PosInOccurrence of the modality of interest.
private Term	term The Term representing the constraint.

Constructor Summary

Constructors

Constructor and Description
ExecutionConstraint(ITreeSettings settings, Node proofNode, PosInOccurrence modalityPIO, Term term) Constructor.

Method Summary

Modifier and Type	Method and Description
java.lang.String	getElementType() Returns a human readable element type name.
PosInOccurrence	getModalityPIO() Returns the PosInOccurrence of the modality of interest including updates.
Term	getTerm() Returns the Term representing the constraint.
protected java.lang.String	lazyComputeName() Computes the name of this node lazily when AbstractExecutionElement.getName() is called the first time.

Methods inherited from class de.uka.ilkd.key.symbolic_execution.model.impl.AbstractExecutionElement

formatTerm, getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, isNameComputed, setName, 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.IExecutionElement

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

Field Detail

term

private final Term term

The Term representing the constraint.

modalityPIO

private final PosInOccurrence modalityPIO

The PosInOccurrence of the modality of interest.

Constructor Detail

ExecutionConstraint

public ExecutionConstraint(ITreeSettings settings,
                           Node proofNode,
                           PosInOccurrence modalityPIO,
                           Term term)

Constructor.

Parameters:

settings - The ITreeSettings to use.

proofNode - The Node of KeY's proof tree which is represented by this IExecutionNode.

term - The Term representing the constraint.

Method Detail

lazyComputeName

protected java.lang.String lazyComputeName()
                                    throws ProofInputException

Computes the name of this node lazily when AbstractExecutionElement.getName() is called the first time.

Specified by:

lazyComputeName in class AbstractExecutionElement

Returns:

The human readable name of this IExecutionNode.

Throws:

ProofInputException

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.

getTerm

public Term getTerm()

Returns the Term representing the constraint.

Specified by:

getTerm in interface IExecutionConstraint

Returns:

The Term representing the constraint.

getModalityPIO

public PosInOccurrence getModalityPIO()

Returns the PosInOccurrence of the modality of interest including updates.

Specified by:

getModalityPIO in interface IExecutionElement

Returns:

The PosInOccurrence of the modality of interest including updates.