IExecutionElement (KeY API Documentation)

All Known Subinterfaces:

IExecutionAuxiliaryContract, IExecutionBaseMethodReturn<S>, IExecutionBlockStartNode<S>, IExecutionBranchCondition, IExecutionBranchStatement, IExecutionConstraint, IExecutionExceptionalMethodReturn, IExecutionJoin, IExecutionLoopCondition, IExecutionLoopInvariant, IExecutionLoopStatement, IExecutionMethodCall, IExecutionMethodReturn, IExecutionMethodReturnValue, IExecutionNode<S>, IExecutionOperationContract, IExecutionStart, IExecutionStatement, IExecutionTermination, IExecutionValue, IExecutionVariable

All Known Implementing Classes:

AbstractExecutionBlockStartNode, AbstractExecutionElement, AbstractExecutionMethodReturn, AbstractExecutionNode, AbstractExecutionValue, AbstractExecutionVariable, ExecutionAllArrayIndicesVariable, ExecutionAuxiliaryContract, ExecutionBranchCondition, ExecutionBranchStatement, ExecutionConstraint, ExecutionExceptionalMethodReturn, ExecutionJoin, ExecutionLoopCondition, ExecutionLoopInvariant, ExecutionLoopStatement, ExecutionMethodCall, ExecutionMethodReturn, ExecutionMethodReturnValue, ExecutionNodeReader.AbstractKeYlessBaseExecutionNode, ExecutionNodeReader.AbstractKeYlessExecutionBlockStartNode, ExecutionNodeReader.AbstractKeYlessExecutionElement, ExecutionNodeReader.AbstractKeYlessExecutionNode, ExecutionNodeReader.KeYlessBlockContract, ExecutionNodeReader.KeYlessBranchCondition, ExecutionNodeReader.KeYlessBranchStatement, ExecutionNodeReader.KeYlessConstraint, ExecutionNodeReader.KeYlessExceptionalMethodReturn, ExecutionNodeReader.KeYlessJoin, ExecutionNodeReader.KeYlessLoopCondition, ExecutionNodeReader.KeYlessLoopInvariant, ExecutionNodeReader.KeYlessLoopStatement, ExecutionNodeReader.KeYlessMethodCall, ExecutionNodeReader.KeYlessMethodReturn, ExecutionNodeReader.KeYlessMethodReturnValue, ExecutionNodeReader.KeYlessOperationContract, ExecutionNodeReader.KeYlessStart, ExecutionNodeReader.KeYlessStatement, ExecutionNodeReader.KeYlessTermination, ExecutionNodeReader.KeYlessValue, ExecutionNodeReader.KeYlessVariable, ExecutionOperationContract, ExecutionStart, ExecutionStatement, ExecutionTermination, ExecutionValue, ExecutionVariable, ExecutionVariableExtractor.ExtractedExecutionValue, ExecutionVariableExtractor.ExtractedExecutionVariable, ExecutionVariableExtractor.StateExecutionVariable
```
public interface IExecutionElement
```
Defines the basic methods and properties each element in the symbolic execution tree model has.

Author:

Martin Hentschel

Method Summary

All Methods Instance Methods Abstract Methods
Modifier and Type	Method and Description
`RuleApp`	`getAppliedRuleApp()` Returns the applied `RuleApp`.
`java.lang.String`	`getElementType()` Returns a human readable element type name.
`InitConfig`	`getInitConfig()` Returns the `InitConfig` used by `getProof()`.
`PosInOccurrence`	`getModalityPIO()` Returns the `PosInOccurrence` of the modality of interest including updates.
`java.lang.String`	`getName()` Returns a human readable name which describes this element.
`Proof`	`getProof()` Returns the `Proof` from which the symbolic execution tree was extracted.
`Node`	`getProofNode()` Returns the `Node` in KeY's proof tree which is represented by this execution tree node.
`NodeInfo`	`getProofNodeInfo()` Returns the `NodeInfo` of `getProofNode()`.
`Services`	`getServices()` Returns the `Services` used by `getProof()`.
`ITreeSettings`	`getSettings()` Returns the `ITreeSettings` to use.
`boolean`	`isDisposed()` Checks if the proof is disposed.

- Method Detail
  - getSettings
```
ITreeSettings getSettings()
```
    Returns the ITreeSettings to use.
    
    Returns:
    
    The ITreeSettings to use.
  - getServices
```
Services getServices()
```
    Returns the Services used by getProof().
    
    Returns:
    
    The Services used by getProof().
  - getInitConfig
```
InitConfig getInitConfig()
```
    Returns the InitConfig used by getProof().
    
    Returns:
    
    The InitConfig used by getProof().
  - getProof
```
Proof getProof()
```
    Returns the Proof from which the symbolic execution tree was extracted.
    
    Returns:
    
    The Proof from which the symbolic execution tree was extracted.
  - getProofNode
```
Node getProofNode()
```
    Returns the Node in KeY's proof tree which is represented by this execution tree node.
    
    Returns:
    
    The Node in KeY's proof tree which is represented by this execution tree node.
  - getAppliedRuleApp
```
RuleApp getAppliedRuleApp()
```
    Returns the applied RuleApp.
    
    Returns:
    
    The applied RuleApp.
  - getModalityPIO
```
PosInOccurrence getModalityPIO()
```
    Returns the PosInOccurrence of the modality of interest including updates.
    
    Returns:
    
    The PosInOccurrence of the modality of interest including updates.
  - getProofNodeInfo
```
NodeInfo getProofNodeInfo()
```
    Returns the NodeInfo of getProofNode().
    
    Returns:
    
    The NodeInfo of getProofNode().
  - getName
```
java.lang.String getName()
                  throws ProofInputException
```
    Returns a human readable name which describes this element.
    
    Returns:
    
    The human readable name which describes this element.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - getElementType
```
java.lang.String getElementType()
```
    Returns a human readable element type name.
    
    Returns:
    
    The human readable element type.
  - isDisposed
```
boolean isDisposed()
```
    Checks if the proof is disposed.
    
    Returns:
    
    true proof is disposed, false proof is not disposed and still valid.

Interface IExecutionElement

Method Summary

Method Detail

getSettings

getServices

getInitConfig

getProof

getProofNode

getAppliedRuleApp

getModalityPIO

getProofNodeInfo

getName

getElementType

isDisposed