de.uka.ilkd.key.rule.inst

Class ContextInstantiationEntry

java.lang.Object

de.uka.ilkd.key.rule.inst.InstantiationEntry<ContextStatementBlockInstantiation>

de.uka.ilkd.key.rule.inst.ContextInstantiationEntry

public class ContextInstantiationEntry
extends InstantiationEntry<ContextStatementBlockInstantiation>

This class is used to store the information about a matched context of a dl formula. (the pi and omega part) TODO: Check if there is a need for ContextStatementBlockInstantiation or if it could be unified with this class

Constructor Summary

Constructors

Constructor and Description
ContextInstantiationEntry(PosInProgram pi, PosInProgram omega, ExecutionContext activeStatementContext, ProgramElement pe) creates a new ContextInstantiationEntry

Method Summary

Modifier and Type	Method and Description
ExecutionContext	activeStatementContext() returns the execution context of the first active statement or null if match is performed outer most
ProgramElement	contextProgram() returns the context program with an ignorable part between prefix and suffix position
PosInProgram	prefix() returns the position of the first statement after the prefix
PosInProgram	suffix() returns the position of the statement just before the suffix starts
java.lang.String	toString() toString

Methods inherited from class de.uka.ilkd.key.rule.inst.InstantiationEntry

equals, getInstantiation, hashCode

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Constructor Detail

ContextInstantiationEntry

ContextInstantiationEntry(PosInProgram pi,
                          PosInProgram omega,
                          ExecutionContext activeStatementContext,
                          ProgramElement pe)

creates a new ContextInstantiationEntry

Parameters:

pi - the PosInProgram describing the position of the first statement after the prefix

omega - the PosInProgram describing the position of the statement just before the suffix starts

activeStatementContext - the ExecutionContext of the first active statement

pe - the ProgramElement the context positions are related to

Method Detail

prefix

public PosInProgram prefix()

returns the position of the first statement after the prefix

Returns:

the position of the first statement after the prefix

suffix

public PosInProgram suffix()

returns the position of the statement just before the suffix starts

Returns:

the position of the statement just before the suffix starts

contextProgram

public ProgramElement contextProgram()

returns the context program with an ignorable part between prefix and suffix position

activeStatementContext

public ExecutionContext activeStatementContext()

returns the execution context of the first active statement or null if match is performed outer most

toString

public java.lang.String toString()

toString

Overrides:

toString in class InstantiationEntry<ContextStatementBlockInstantiation>