| java.lang.Object de.uka.ilkd.key.rule.inst.InstantiationEntry de.uka.ilkd.key.rule.inst.ContextInstantiationEntry
ContextInstantiationEntry | public class ContextInstantiationEntry extends InstantiationEntry (Code) | | This class is used to store the information about a matched
context of a dl formula. (the pi and omega part)
|
ContextInstantiationEntry | ContextInstantiationEntry(SchemaVariable ctxt, PosInProgram pi, PosInProgram omega, ExecutionContext activeStatementContext, ProgramElement pe)(Code) | | creates a new ContextInstantiationEntry
Parameters: ctxt - the SchemaVariable that isinstantiated Parameters: pi - the PosInProgram describing the positionof the first statement after the prefix Parameters: omega - the PosInProgram describing the positionof the statement just before the suffix starts Parameters: activeStatementContext - the ExecutionContext of the firstactive statement Parameters: pe - the ProgramElement the context positions are related to |
activeStatementContext | public ExecutionContext activeStatementContext()(Code) | | returns the execution context of the first active statement or
null if match is performed outer most
|
contextProgram | public ProgramElement contextProgram()(Code) | | returns the context program with an ignorable part between prefix
and suffix position
|
getInstantiation | public Object getInstantiation()(Code) | | returns the instantiation of the SchemaVariable
the instantiation of the SchemaVariable |
prefix | public PosInProgram prefix()(Code) | | returns the position of the first statement after the prefix
the position of the first statement after the prefix |
suffix | public PosInProgram suffix()(Code) | | returns the position of the statement just before the suffix
starts
the position of the statement just before the suffixstarts |
|
|