de.uka.ilkd.key.symbolic_execution

Class ExecutionNodeReader.KeYlessConstraint

java.lang.Object

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

de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.KeYlessConstraint

All Implemented Interfaces:

IExecutionConstraint, IExecutionElement

Enclosing class:

ExecutionNodeReader

public static class ExecutionNodeReader.KeYlessConstraint
extends ExecutionNodeReader.AbstractKeYlessExecutionElement
implements IExecutionConstraint

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

Author:

Martin Hentschel

Constructor Summary

Constructors

Constructor and Description
KeYlessConstraint(java.lang.String name) 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.

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.IExecutionElement

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

Constructor Detail

KeYlessConstraint

public KeYlessConstraint(java.lang.String name)

Constructor.

Parameters:

name - The name.

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.

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.